Loogle!

Result

Found 4371 declarations mentioning IsScalarTower. Of these, 3585 match your pattern(s). Of these, only the first 200 are shown.

• IsScalarTower.op_right 📋 Mathlib.Algebra.Group.Action.Defs
  {M : Type u_1} {N : Type u_2} {α : Type u_5} [SMul M α] [SMul M N] [SMul N α] [SMul Nᵐᵒᵖ α] [IsCentralScalar N α] [IsScalarTower M N α] : IsScalarTower M Nᵐᵒᵖ α
• SMul.comp.isScalarTower 📋 Mathlib.Algebra.Group.Action.Defs
  {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [SMul α β] [IsScalarTower M α β] (g : N → M) : IsScalarTower N α β
• IsScalarTower.op_left 📋 Mathlib.Algebra.Group.Action.Defs
  {M : Type u_1} {N : Type u_2} {α : Type u_5} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [SMul M N] [SMul Mᵐᵒᵖ N] [IsCentralScalar M N] [SMul N α] [IsScalarTower M N α] : IsScalarTower Mᵐᵒᵖ N α
• Commute.smul_left 📋 Mathlib.Algebra.Group.Action.Defs
  {M : Type u_1} {α : Type u_5} [SMul M α] [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a b : α} (h : Commute a b) (r : M) : Commute (r • a) b
• Commute.smul_right 📋 Mathlib.Algebra.Group.Action.Defs
  {M : Type u_1} {α : Type u_5} [SMul M α] [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a b : α} (h : Commute a b) (r : M) : Commute a (r • b)
• smul_mul_assoc 📋 Mathlib.Algebra.Group.Action.Defs
  {α : Type u_5} {β : Type u_6} [Mul β] [SMul α β] [IsScalarTower α β β] (r : α) (x y : β) : r • x * y = r • (x * y)
• smul_assoc 📋 Mathlib.Algebra.Group.Action.Defs
  {α : Type u_5} {M : Type u_9} {N : Type u_10} [SMul M N] [SMul N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : N) (z : α) : (x • y) • z = x • y • z
• IsScalarTower.smul_assoc 📋 Mathlib.Algebra.Group.Action.Defs
  {M : Type u_9} {N : Type u_10} {α : Type u_11} {inst✝ : SMul M N} {inst✝¹ : SMul N α} {inst✝² : SMul M α} [self : IsScalarTower M N α] (x : M) (y : N) (z : α) : (x • y) • z = x • y • z
• smul_one_mul 📋 Mathlib.Algebra.Group.Action.Defs
  {M : Type u_9} {N : Type u_10} [MulOneClass N] [SMul M N] [IsScalarTower M N N] (x : M) (y : N) : x • 1 * y = x • y
• SMulCommClass.of_commMonoid 📋 Mathlib.Algebra.Group.Action.Defs
  (A : Type u_9) (B : Type u_10) (G : Type u_11) [CommMonoid G] [SMul A G] [SMul B G] [IsScalarTower A G G] [IsScalarTower B G G] : SMulCommClass A B G
• smul_div_assoc 📋 Mathlib.Algebra.Group.Action.Defs
  {α : Type u_5} {β : Type u_6} [DivInvMonoid β] [SMul α β] [IsScalarTower α β β] (r : α) (x y : β) : r • x / y = r • (x / y)
• IsScalarTower.to₁₂₄ 📋 Mathlib.Algebra.Group.Action.Defs
  (M : Type u_9) (N : Type u_10) (P : Type u_11) (Q : Type u_12) [SMul M N] [SMul M P] [SMul M Q] [SMul N P] [SMul N Q] [Monoid P] [MulAction P Q] [IsScalarTower M N P] [IsScalarTower M P Q] [IsScalarTower N P Q] : IsScalarTower M N Q
• smul_one_smul 📋 Mathlib.Algebra.Group.Action.Defs
  {α : Type u_5} {M : Type u_9} (N : Type u_10) [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : α) : (x • 1) • y = x • y
• mul_smul_mul_comm 📋 Mathlib.Algebra.Group.Action.Defs
  {α : Type u_5} {β : Type u_6} [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β] [IsScalarTower α α β] [SMulCommClass α β β] (a b : α) (c d : β) : (a * b) • (c * d) = a • c * b • d
• smul_mul_smul 📋 Mathlib.Algebra.Group.Action.Defs
  {α : Type u_5} {β : Type u_6} [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β] [IsScalarTower α α β] [SMulCommClass α β β] (a : α) (b : β) (c : α) (d : β) : a • b * c • d = (a * c) • (b * d)
• smul_mul_smul_comm 📋 Mathlib.Algebra.Group.Action.Defs
  {α : Type u_5} {β : Type u_6} [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β] [IsScalarTower α α β] [SMulCommClass α β β] (a : α) (b : β) (c : α) (d : β) : a • b * c • d = (a * c) • (b * d)
• IsScalarTower.to₁₃₄ 📋 Mathlib.Algebra.Group.Action.Defs
  (M : Type u_9) (N : Type u_10) (P : Type u_11) (Q : Type u_12) [SMul M N] [SMul M P] [SMul M Q] [SMul P Q] [Monoid N] [MulAction N P] [MulAction N Q] [IsScalarTower M N P] [IsScalarTower M N Q] [IsScalarTower N P Q] : IsScalarTower M P Q
• smul_smul_smul_comm 📋 Mathlib.Algebra.Group.Action.Defs
  {α : Type u_5} {β : Type u_6} {γ : Type u_7} {δ : Type u_8} [SMul α β] [SMul α γ] [SMul β δ] [SMul α δ] [SMul γ δ] [IsScalarTower α β δ] [IsScalarTower α γ δ] [SMulCommClass β γ δ] (a : α) (b : β) (c : γ) (d : δ) : (a • b) • c • d = (a • c) • b • d
• IsScalarTower.to₂₃₄ 📋 Mathlib.Algebra.Group.Action.Defs
  (M : Type u_9) (N : Type u_10) (P : Type u_11) (Q : Type u_12) [SMul M N] [SMul M P] [SMul M Q] [SMul P Q] [Monoid N] [MulAction N P] [MulAction N Q] [IsScalarTower M N P] [IsScalarTower M N Q] [IsScalarTower M P Q] (h : Function.Surjective fun m => m • 1) : IsScalarTower N P Q
• Commute.smul_left_iff 📋 Mathlib.Algebra.Group.Action.Defs
  {G : Type u_3} {H : Type u_4} [Group G] {g : G} [Mul H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] {a b : H} : Commute (g • a) b ↔ Commute a b
• Commute.smul_right_iff 📋 Mathlib.Algebra.Group.Action.Defs
  {G : Type u_3} {H : Type u_4} [Group G] {g : G} [Mul H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] {a b : H} : Commute a (g • b) ↔ Commute a b
• smul_pow 📋 Mathlib.Algebra.Group.Action.Defs
  {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N] (r : M) (x : N) (n : ℕ) : (r • x) ^ n = r ^ n • x ^ n
• smul_inv 📋 Mathlib.Algebra.Group.Action.Defs
  {G : Type u_3} {H : Type u_4} [Group G] [Group H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] (g : G) (a : H) : (g • a)⁻¹ = g⁻¹ • a⁻¹
• smul_zpow 📋 Mathlib.Algebra.Group.Action.Defs
  {G : Type u_3} {H : Type u_4} [Group G] [Group H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] (g : G) (a : H) (n : ℤ) : (g • a) ^ n = g ^ n • a ^ n
• faithfulSMul_iff_injective_smul_one 📋 Mathlib.Algebra.Group.Action.Faithful
  (R : Type u_4) (A : Type u_5) [MulOneClass A] [SMul R A] [IsScalarTower R A A] : FaithfulSMul R A ↔ Function.Injective fun r => r • 1
• IsScalarTower.to₁₂₃ 📋 Mathlib.Algebra.Group.Action.Faithful
  (M : Type u_4) (N : Type u_5) (P : Type u_6) (Q : Type u_7) [SMul M N] [SMul M P] [SMul M Q] [SMul N P] [SMul N Q] [SMul P Q] [FaithfulSMul P Q] [IsScalarTower M N Q] [IsScalarTower M P Q] [IsScalarTower N P Q] : IsScalarTower M N P
• FaithfulSMul.tower_bot 📋 Mathlib.Algebra.Group.Action.Faithful
  (R : Type u_4) (S : Type u_5) (T : Type u_6) [Monoid S] [MulOneClass T] [SMul R S] [SMul R T] [MulAction S T] [IsScalarTower R S S] [IsScalarTower R T T] [IsScalarTower R S T] [FaithfulSMul R T] : FaithfulSMul R S
• FaithfulSMul.trans 📋 Mathlib.Algebra.Group.Action.Faithful
  (R : Type u_4) (S : Type u_5) (T : Type u_6) [Monoid S] [MulOneClass T] [SMul R S] [IsScalarTower R S S] [MulAction S T] [IsScalarTower S T T] [SMul R T] [IsScalarTower R T T] [IsScalarTower R S T] [FaithfulSMul R S] [FaithfulSMul S T] : FaithfulSMul R T
• SMulCommClass.opposite_mid 📋 Mathlib.Algebra.Group.Action.Opposite
  {M : Type u_5} {N : Type u_6} [Mul N] [SMul M N] [IsScalarTower M N N] : SMulCommClass M Nᵐᵒᵖ N
• MulOpposite.instIsScalarTower 📋 Mathlib.Algebra.Group.Action.Opposite
  {M : Type u_1} {N : Type u_2} {α : Type u_3} [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] : IsScalarTower M N αᵐᵒᵖ
• smul_inv₀ 📋 Mathlib.Algebra.GroupWithZero.Action.Defs
  {G₀ : Type u_4} {G₀' : Type u_5} [GroupWithZero G₀] [GroupWithZero G₀'] [MulActionWithZero G₀ G₀'] [SMulCommClass G₀ G₀' G₀'] [IsScalarTower G₀ G₀' G₀'] (c : G₀) (x : G₀') : (c • x)⁻¹ = c⁻¹ • x⁻¹
• Units.instIsScalarTower 📋 Mathlib.Algebra.Group.Action.Units
  {M : Type u_3} {N : Type u_4} {α : Type u_5} [Monoid M] [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] : IsScalarTower Mˣ N α
• IsUnit.smul 📋 Mathlib.Algebra.Group.Action.Units
  {G : Type u_1} {M : Type u_3} [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] {m : M} (g : G) (h : IsUnit m) : IsUnit (g • m)
• Units.isScalarTower'_left 📋 Mathlib.Algebra.Group.Action.Units
  {G : Type u_1} {M : Type u_3} {α : Type u_5} [Group G] [Monoid M] [MulAction G M] [SMul M α] [SMul G α] [SMulCommClass G M M] [IsScalarTower G M M] [IsScalarTower G M α] : IsScalarTower G Mˣ α
• Units.val_smul 📋 Mathlib.Algebra.Group.Action.Units
  {G : Type u_1} {M : Type u_3} [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] (g : G) (m : Mˣ) : ↑(g • m) = g • ↑m
• Units.smul_inv 📋 Mathlib.Algebra.Group.Action.Units
  {G : Type u_1} {M : Type u_3} [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] (g : G) (m : Mˣ) : (g • m)⁻¹ = g⁻¹ • m⁻¹
• Units.mulAction'.eq_1 📋 Mathlib.Algebra.Group.Action.Units
  {G : Type u_1} {M : Type u_3} [Group G] [Monoid M] [MulAction G M] [SMulCommClass G M M] [IsScalarTower G M M] : Units.mulAction' = { smul := fun g m => { val := g • ↑m, inv := g⁻¹ • ↑m⁻¹, val_inv := ⋯, inv_val := ⋯ }, mul_smul := ⋯, one_smul := ⋯ }
• Units.smulCommClass' 📋 Mathlib.Algebra.Group.Action.Units
  {G : Type u_1} {H : Type u_2} {M : Type u_3} [Group G] [Group H] [Monoid M] [MulAction G M] [SMulCommClass G M M] [MulAction H M] [SMulCommClass H M M] [IsScalarTower G M M] [IsScalarTower H M M] [SMulCommClass G H M] : SMulCommClass G H Mˣ
• Units.isScalarTower' 📋 Mathlib.Algebra.Group.Action.Units
  {G : Type u_1} {H : Type u_2} {M : Type u_3} [SMul G H] [Group G] [Group H] [Monoid M] [MulAction G M] [SMulCommClass G M M] [MulAction H M] [SMulCommClass H M M] [IsScalarTower G M M] [IsScalarTower H M M] [IsScalarTower G H M] : IsScalarTower G H Mˣ
• isUnit_smul_iff 📋 Mathlib.Algebra.Group.Action.Basic
  {α : Type u_5} {β : Type u_6} [Group α] [Monoid β] [MulAction α β] [SMulCommClass α β β] [IsScalarTower α β β] (g : α) (m : β) : IsUnit (g • m) ↔ IsUnit m
• MulAction.IsPretransitive.of_isScalarTower 📋 Mathlib.Algebra.Group.Action.Pretransitive
  (M : Type u_5) {N : Type u_6} {α : Type u_7} [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] [MulAction.IsPretransitive M α] : MulAction.IsPretransitive N α
• MonoidHom.smulOneHom_apply 📋 Mathlib.Algebra.Group.Action.Hom
  {M : Type u_4} {N : Type u_5} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] (x : M) : MonoidHom.smulOneHom x = x • 1
• MonoidHom.smulOneHom.eq_1 📋 Mathlib.Algebra.Group.Action.Hom
  {M : Type u_4} {N : Type u_5} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] : MonoidHom.smulOneHom = { toFun := fun x => x • 1, map_one' := ⋯, map_mul' := ⋯ }
• Submonoid.instIsScalarTowerSubtypeMem 📋 Mathlib.Algebra.Group.Submonoid.MulAction
  {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [SetLike S' M'] (s : S') [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] : IsScalarTower (↥s) α β
• Submonoid.isScalarTower 📋 Mathlib.Algebra.Group.Submonoid.MulAction
  {M' : Type u_1} {α : Type u_2} {β : Type u_3} [MulOneClass M'] [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] (S : Submonoid M') : IsScalarTower (↥S) α β
• Set.isScalarTower 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Set γ)
• Set.isScalarTower' 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α (Set β) (Set γ)
• Set.isScalarTower'' 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower (Set α) (Set β) (Set γ)
• Submonoid.pow_smul_mem_closure_smul 📋 Mathlib.Algebra.Group.Submonoid.Pointwise
  {M : Type u_3} [Monoid M] {N : Type u_7} [CommMonoid N] [MulAction M N] [IsScalarTower M N N] (r : M) (s : Set N) {x : N} (hx : x ∈ Submonoid.closure s) : ∃ n, r ^ n • x ∈ Submonoid.closure (r • s)
• MulAction.stabilizer_smul_eq_left 📋 Mathlib.GroupTheory.GroupAction.Defs
  {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G α] [MulAction G β] [SMul α β] [IsScalarTower G α β] (a : α) (b : β) (h : Function.Injective fun x => x • b) : MulAction.stabilizer G (a • b) = MulAction.stabilizer G a
• MulAction.le_stabilizer_smul_left 📋 Mathlib.GroupTheory.GroupAction.Defs
  {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [MulAction G α] [MulAction G β] [SMul α β] [IsScalarTower G α β] (a : α) (b : β) : MulAction.stabilizer G a ≤ MulAction.stabilizer G (a • b)
• MulAction.stabilizer_mul_eq_left 📋 Mathlib.GroupTheory.GroupAction.Defs
  {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [Group α] [IsScalarTower G α α] (a b : α) : MulAction.stabilizer G (a * b) = MulAction.stabilizer G a
• ConjAct.unitsSMulCommClass 📋 Mathlib.GroupTheory.GroupAction.ConjAct
  (α : Type u_1) {M : Type u_2} [Monoid M] [SMul α M] [SMulCommClass α M M] [IsScalarTower α M M] : SMulCommClass α (ConjAct Mˣ) M
• ConjAct.unitsSMulCommClass' 📋 Mathlib.GroupTheory.GroupAction.ConjAct
  (α : Type u_1) {M : Type u_2} [Monoid M] [SMul α M] [SMulCommClass M α M] [IsScalarTower α M M] : SMulCommClass (ConjAct Mˣ) α M
• ConjAct.smulCommClass 📋 Mathlib.GroupTheory.GroupAction.ConjAct
  (α : Type u_1) {G : Type u_3} [Group G] [SMul α G] [SMulCommClass α G G] [IsScalarTower α G G] : SMulCommClass α (ConjAct G) G
• ConjAct.smulCommClass' 📋 Mathlib.GroupTheory.GroupAction.ConjAct
  (α : Type u_1) {G : Type u_3} [Group G] [SMul α G] [SMulCommClass G α G] [IsScalarTower α G G] : SMulCommClass (ConjAct G) α G
• OreLocalization.instSMulOfIsScalarTower.congr_simp 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M X] [IsScalarTower R M M] : OreLocalization.instSMulOfIsScalarTower = OreLocalization.instSMulOfIsScalarTower
• OreLocalization.instSMulOfIsScalarTower.eq_1 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M X] [IsScalarTower R M M] : OreLocalization.instSMulOfIsScalarTower = { smul := OreLocalization.hsmul }
• OreLocalization.instIsScalarTower_1 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] : IsScalarTower R (OreLocalization S M) (OreLocalization S X)
• OreLocalization.instSMulCommClass_1 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMulCommClass R M M] : SMulCommClass R (OreLocalization S M) (OreLocalization S X)
• OreLocalization.instSMulCommClass 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMul R' X] [SMul R' M] [IsScalarTower R' M M] [IsScalarTower R' M X] [SMulCommClass R R' M] : SMulCommClass R R' (OreLocalization S X)
• OreLocalization.instIsCentralScalar 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMul Rᵐᵒᵖ M] [SMul Rᵐᵒᵖ X] [IsScalarTower Rᵐᵒᵖ M M] [IsScalarTower Rᵐᵒᵖ M X] [IsCentralScalar R M] : IsCentralScalar R (OreLocalization S X)
• OreLocalization.instIsScalarTower 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMul R' X] [SMul R' M] [IsScalarTower R' M M] [IsScalarTower R' M X] [SMul R R'] [IsScalarTower R R' M] : IsScalarTower R R' (OreLocalization S X)
• OreLocalization.smul_one_smul 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : OreLocalization S X) : (r • 1) • x = r • x
• OreLocalization.instMulActionOfIsScalarTower.eq_1 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] {R : Type u_5} [Monoid R] [MulAction R M] [IsScalarTower R M M] [MulAction R X] [IsScalarTower R M X] : OreLocalization.instMulActionOfIsScalarTower = { toSMul := OreLocalization.instSMulOfIsScalarTower, mul_smul := ⋯, one_smul := ⋯ }
• OreLocalization.smul_oreDiv 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : X) (s : ↥S) : r • (x /ₒ s) = OreLocalization.oreNum (r • 1) s • x /ₒ OreLocalization.oreDenom (r • 1) s
• OreLocalization.smul_oreDiv_one 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : X) : r • (x /ₒ 1) = r • x /ₒ 1
• OreLocalization.smul_one_oreDiv_one_smul 📋 Mathlib.GroupTheory.OreLocalization.Basic
  {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : OreLocalization S X) : (r • 1 /ₒ 1) • x = r • x
• Localization.instSMulCommClassOfIsScalarTower 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
  {R : Type u_7} {M : Type u_8} [CommMonoid M] [SMul R M] [IsScalarTower R M M] : SMulCommClass R M M
• Localization.smul_mk 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
  {M : Type u_1} [CommMonoid M] {S : Submonoid M} {R : Type u_4} [SMul R M] [IsScalarTower R M M] (c : R) (a : M) (b : ↥S) : c • Localization.mk a b = Localization.mk (c • a) b
• Commute.smul_left_iff₀ 📋 Mathlib.Algebra.GroupWithZero.Action.Units
  {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β} (ha : a ≠ 0) : Commute (a • x) y ↔ Commute x y
• Commute.smul_right_iff₀ 📋 Mathlib.Algebra.GroupWithZero.Action.Units
  {α : Type u_4} {β : Type u_5} [GroupWithZero α] [MulAction α β] {a : α} [Mul β] [SMulCommClass α β β] [IsScalarTower α β β] {x y : β} (ha : a ≠ 0) : Commute x (a • y) ↔ Commute x y
• RingHom.smulOneHom_apply 📋 Mathlib.Algebra.Module.RingHom
  {R : Type u_1} {S : Type u_2} [Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] (x : R) : RingHom.smulOneHom x = x • 1
• IsSMulRegular.of_mul 📋 Mathlib.Algebra.Regular.SMul
  {R : Type u_1} {M : Type u_3} {a b : R} [SMul R M] [Mul R] [IsScalarTower R R M] (ab : IsSMulRegular M (a * b)) : IsSMulRegular M b
• IsSMulRegular.of_smul 📋 Mathlib.Algebra.Regular.SMul
  {R : Type u_1} {S : Type u_2} {M : Type u_3} {s : S} [SMul R M] [SMul R S] [SMul S M] [IsScalarTower R S M] (a : R) (ab : IsSMulRegular M (a • s)) : IsSMulRegular M s
• IsSMulRegular.mul 📋 Mathlib.Algebra.Regular.SMul
  {R : Type u_1} {M : Type u_3} {a b : R} [SMul R M] [Mul R] [IsScalarTower R R M] (ra : IsSMulRegular M a) (rb : IsSMulRegular M b) : IsSMulRegular M (a * b)
• IsSMulRegular.mul_iff_right 📋 Mathlib.Algebra.Regular.SMul
  {R : Type u_1} {M : Type u_3} {a b : R} [SMul R M] [Mul R] [IsScalarTower R R M] (ha : IsSMulRegular M a) : IsSMulRegular M (a * b) ↔ IsSMulRegular M b
• IsSMulRegular.smul 📋 Mathlib.Algebra.Regular.SMul
  {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [SMul R M] [SMul R S] [SMul S M] [IsScalarTower R S M] (ra : IsSMulRegular M a) (rs : IsSMulRegular M s) : IsSMulRegular M (a • s)
• IsSMulRegular.smul_iff 📋 Mathlib.Algebra.Regular.SMul
  {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [SMul R M] [SMul R S] [SMul S M] [IsScalarTower R S M] (b : S) (ha : IsSMulRegular M a) : IsSMulRegular M (a • b) ↔ IsSMulRegular M b
• IsSMulRegular.mul_iff 📋 Mathlib.Algebra.Regular.SMul
  {R : Type u_1} {M : Type u_3} {a b : R} [CommSemigroup R] [SMul R M] [IsScalarTower R R M] : IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
• IsSMulRegular.mul_and_mul_iff 📋 Mathlib.Algebra.Regular.SMul
  {R : Type u_1} {M : Type u_3} {a b : R} [SMul R M] [Mul R] [IsScalarTower R R M] : IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
• IsSMulRegular.of_smul_eq_one 📋 Mathlib.Algebra.Regular.SMul
  {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [Monoid S] [SMul R M] [SMul R S] [MulAction S M] [IsScalarTower R S M] (h : a • s = 1) : IsSMulRegular M s
• IsScalarTower.smulHomClass 📋 Mathlib.GroupTheory.GroupAction.Hom
  (M' : Type u_1) (X : Type u_5) [SMul M' X] (Y : Type u_6) [SMul M' Y] (F : Type u_8) [FunLike F X Y] [MulOneClass X] [SMul X Y] [IsScalarTower M' X Y] [MulActionHomClass F X X Y] : MulActionHomClass F M' X Y
• LinearMap.IsScalarTower.compatibleSMul' 📋 Mathlib.Algebra.Module.LinearMap.Defs
  {M : Type u_8} [AddCommMonoid M] {R : Type u_14} {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R S] [IsScalarTower R S M] : LinearMap.CompatibleSMul S M R S
• LinearMap.IsScalarTower.compatibleSMul 📋 Mathlib.Algebra.Module.LinearMap.Defs
  {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_14} {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [SMul R S] [IsScalarTower R S M] [IsScalarTower R S M₂] : LinearMap.CompatibleSMul M M₂ R S
• LinearMap.isScalarTower_of_injective 📋 Mathlib.Algebra.Module.LinearMap.Defs
  {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (R : Type u_14) {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [SMul R S] [LinearMap.CompatibleSMul M M₂ R S] [IsScalarTower R S M₂] (f : M →ₗ[S] M₂) (hf : Function.Injective ⇑f) : IsScalarTower R S M
• LinearMap.mulRight_apply 📋 Mathlib.Algebra.Module.LinearMap.Defs
  (R : Type u_14) {A : Type u_15} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] (a b : A) : (LinearMap.mulRight R a) b = b * a
• LinearMap.mulRight_zero_eq_zero 📋 Mathlib.Algebra.Module.LinearMap.Defs
  (R : Type u_14) (A : Type u_15) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] : LinearMap.mulRight R 0 = 0
• LinearMap.mulLeftRight_apply 📋 Mathlib.Algebra.Module.LinearMap.Defs
  {R : Type u_14} {A : Type u_15} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a b x : A) : (LinearMap.mulLeftRight R (a, b)) x = a * x * b
• LinearMap.instIsScalarTower 📋 Mathlib.Algebra.Module.LinearMap.Defs
  {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {T : Type u_7} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] [SMul S T] [IsScalarTower S T M₂] : IsScalarTower S T (M →ₛₗ[σ₁₂] M₂)
• LinearMap.mulRight_toAddMonoidHom 📋 Mathlib.Algebra.Module.LinearMap.Defs
  (R : Type u_14) {A : Type u_15} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] (a : A) : ↑(LinearMap.mulRight R a) = AddMonoidHom.mulRight a
• LinearMap.toAddMonoidHom_mulRight 📋 Mathlib.Algebra.Module.LinearMap.Defs
  (R : Type u_14) {A : Type u_15} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] (a : A) : ↑(LinearMap.mulRight R a) = AddMonoidHom.mulRight a
• algebraMap.coe_smul 📋 Mathlib.Algebra.Algebra.Defs
  {A : Type u_1} {B : Type u_2} (a : A) (b : B) (C : Type u_3) [SMul A B] [CommSemiring B] [Semiring C] [Algebra B C] [SMul A C] [IsScalarTower A B C] : ↑(a • b) = a • ↑b
• Prod.isScalarTower 📋 Mathlib.Algebra.Group.Action.Prod
  {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [SMul M N] [IsScalarTower M N α] [IsScalarTower M N β] : IsScalarTower M N (α × β)
• Prod.isScalarTowerBoth 📋 Mathlib.Algebra.Group.Action.Prod
  {M : Type u_1} {N : Type u_2} {P : Type u_3} [Mul N] [Mul P] [SMul M N] [SMul M P] [IsScalarTower M N N] [IsScalarTower M P P] : IsScalarTower M (N × P) (N × P)
• smulMulHom_apply 📋 Mathlib.Algebra.Group.Action.Prod
  {α : Type u_5} {β : Type u_6} [Monoid α] [Mul β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (a : α × β) : smulMulHom a = a.1 • a.2
• smulMonoidHom_apply 📋 Mathlib.Algebra.Group.Action.Prod
  {α : Type u_5} {β : Type u_6} [Monoid α] [MulOneClass β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (a✝ : α × β) : smulMonoidHom a✝ = smulMulHom.toFun a✝
• smulMonoidWithZeroHom_apply 📋 Mathlib.Algebra.GroupWithZero.Action.Basic
  {M₀ : Type u_5} {N₀ : Type u_6} [MonoidWithZero M₀] [MulZeroOneClass N₀] [MulActionWithZero M₀ N₀] [IsScalarTower M₀ N₀ N₀] [SMulCommClass M₀ N₀ N₀] (a✝ : M₀ × N₀) : smulMonoidWithZeroHom a✝ = (↑smulMonoidHom).toFun a✝
• IsUnit.smul_sub_iff_sub_inv_smul 📋 Mathlib.Algebra.GroupWithZero.Action.Basic
  {G : Type u_1} {R : Type u_7} [Group G] [Monoid R] [AddGroup R] [DistribMulAction G R] [IsScalarTower G R R] [SMulCommClass G R R] (r : G) (a : R) : IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
• ZeroHom.instIsScalarTower 📋 Mathlib.Algebra.GroupWithZero.Action.Hom
  {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [Zero A] [Zero B] [SMul M N] [SMulZeroClass M B] [SMulZeroClass N B] [IsScalarTower M N B] : IsScalarTower M N (ZeroHom A B)
• AddMonoidHom.instIsScalarTower 📋 Mathlib.Algebra.GroupWithZero.Action.Hom
  {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [AddZeroClass A] [AddZeroClass B] [SMul M N] [DistribSMul M B] [DistribSMul N B] [IsScalarTower M N B] : IsScalarTower M N (A →+ B)
• AddMonoid.End.isScalarTower 📋 Mathlib.Algebra.Module.Hom
  {R : Type u_1} {S : Type u_2} {A : Type u_4} [Monoid R] [Monoid S] [AddCommMonoid A] [DistribMulAction R A] [DistribMulAction S A] [SMul R S] [IsScalarTower R S A] : IsScalarTower R S (AddMonoid.End A)
• LinearMap.mulRight.congr_simp 📋 Mathlib.Algebra.Module.LinearMap.Basic
  (R : Type u_14) {A : Type u_15} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] (b b✝ : A) (e_b : b = b✝) : LinearMap.mulRight R b = LinearMap.mulRight R b✝
• LinearMap.mulRight_inj 📋 Mathlib.Algebra.Module.LinearMap.Basic
  {R : Type u_6} {A : Type u_7} [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] {a b : A} : LinearMap.mulRight R a = LinearMap.mulRight R b ↔ a = b
• LinearMap.mulRight_one 📋 Mathlib.Algebra.Module.LinearMap.Basic
  (R : Type u_6) (A : Type u_7) [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] : LinearMap.mulRight R 1 = LinearMap.id
• LinearMap.mulRight_mul 📋 Mathlib.Algebra.Module.LinearMap.Basic
  (R : Type u_6) (A : Type u_7) [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] (a b : A) : LinearMap.mulRight R (a * b) = LinearMap.mulRight R b ∘ₗ LinearMap.mulRight R a
• LinearMap.mulRight_eq_zero_iff 📋 Mathlib.Algebra.Module.LinearMap.Basic
  (R : Type u_6) (A : Type u_7) [Semiring R] [NonAssocSemiring A] [Module R A] [IsScalarTower R A A] (a : A) : LinearMap.mulRight R a = 0 ↔ a = 0
• Module.End.apply_smulCommClass 📋 Mathlib.Algebra.Module.LinearMap.End
  {R : Type u_1} {S : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass S (Module.End R M) M
• Module.End.apply_smulCommClass' 📋 Mathlib.Algebra.Module.LinearMap.End
  {R : Type u_1} {S : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass (Module.End R M) S M
• LinearMap.smulRight_zero 📋 Mathlib.Algebra.Module.LinearMap.End
  {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f : M₁ →ₗ[R] S) : f.smulRight 0 = 0
• LinearMap.smulRight.congr_simp 📋 Mathlib.Algebra.Module.LinearMap.End
  {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f f✝ : M₁ →ₗ[R] S) (e_f : f = f✝) (x x✝ : M) (e_x : x = x✝) : f.smulRight x = f✝.smulRight x✝
• LinearMap.zero_smulRight 📋 Mathlib.Algebra.Module.LinearMap.End
  {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (x : M) : LinearMap.smulRight 0 x = 0
• Module.End.instSMulCommClass 📋 Mathlib.Algebra.Module.LinearMap.End
  {R : Type u_1} {S : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M] : SMulCommClass S (Module.End R M) (Module.End R M)
• Module.End.instSMulCommClass' 📋 Mathlib.Algebra.Module.LinearMap.End
  {R : Type u_1} {S : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] [SMul S R] [IsScalarTower S R M] : SMulCommClass (Module.End R M) S (Module.End R M)
• LinearMap.coe_smulRight 📋 Mathlib.Algebra.Module.LinearMap.End
  {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f : M₁ →ₗ[R] S) (x : M) : ⇑(f.smulRight x) = fun c => f c • x
• LinearMap.smulRight_apply 📋 Mathlib.Algebra.Module.LinearMap.End
  {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] (f : M₁ →ₗ[R] S) (x : M) (c : M₁) : (f.smulRight x) c = f c • x
• LinearMap.smulRight_apply_eq_zero_iff 📋 Mathlib.Algebra.Module.LinearMap.End
  {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] [Semiring S] [Module R S] [Module S M] [IsScalarTower R S M] {f : M₁ →ₗ[R] S} {x : M} [NoZeroSMulDivisors S M] : f.smulRight x = 0 ↔ f = 0 ∨ x = 0
• LinearEquiv.apply_smulCommClass 📋 Mathlib.Algebra.Module.Equiv.Basic
  {R : Type u_1} {S : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass S (M ≃ₗ[R] M) M
• LinearEquiv.apply_smulCommClass' 📋 Mathlib.Algebra.Module.Equiv.Basic
  {R : Type u_1} {S : Type u_4} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass (M ≃ₗ[R] M) S M
• Subgroup.instIsScalarTowerSubtypeMem 📋 Mathlib.Algebra.Group.Subgroup.Actions
  {G : Type u_1} {α : Type u_2} {β : Type u_3} [Group G] [SMul α β] [MulAction G α] [MulAction G β] [IsScalarTower G α β] (S : Subgroup G) : IsScalarTower (↥S) α β
• SMulMemClass.ofIsScalarTower 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  (S : Type u_1) (M : Type u_2) (N : Type u_3) (α : Type u_4) [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] : SMulMemClass S M α
• SetLike.instIsScalarTower 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {R : Type u} {M : Type v} [SMul R M] [SetLike S M] [hS : SMulMemClass S R M] [Mul M] [MulMemClass S M] [IsScalarTower R M M] (s : S) : IsScalarTower R ↥s ↥s
• SetLike.instIsScalarTowerSubtypeMem 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) : IsScalarTower M N ↥s
• SetLike.instSMulCommClassSubtypeMem_1 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) [SMulCommClass M N α] : SMulCommClass M N ↥s
• SetLike.instSMulCommClassSubtypeMem_2 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) [SMulCommClass N M α] : SMulCommClass N M ↥s
• SubMulAction.isScalarTower 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) : IsScalarTower S R ↥p
• SubMulAction.isCentralScalar 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S ↥p
• SubMulAction.smul_of_tower_mem 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) (s : S) {x : M} (h : x ∈ p) : s • x ∈ p
• SubMulAction.isScalarTower' 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) {S' : Type u_1} [SMul S' R] [SMul S' S] [SMul S' M] [IsScalarTower S' R M] [IsScalarTower S' S M] : IsScalarTower S' S ↥p
• SetLike.val_smul_of_tower 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) (r : M) (x : ↥s) : ↑(r • x) = r • ↑x
• SetLike.smul'.eq_1 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) : SetLike.smul' s = { smul := fun r x => ⟨r • ↑x, ⋯⟩ }
• SubMulAction.smul_mem_iff' 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {R : Type u} {M : Type v} [Monoid R] [MulAction R M] (p : SubMulAction R M) {G : Type u_1} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] (g : G) {x : M} : g • x ∈ p ↔ x ∈ p
• SubMulAction.smul_mem_iff 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {R : Type u} {M : Type v} [GroupWithZero S] [Monoid R] [MulAction R M] [SMul S R] [MulAction S M] [IsScalarTower S R M] (p : SubMulAction R M) {s : S} {x : M} (s0 : s ≠ 0) : s • x ∈ p ↔ x ∈ p
• SubMulAction.mulAction'.eq_1 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M] (p : SubMulAction R M) : p.mulAction' = { toSMul := p.smul', mul_smul := ⋯, one_smul := ⋯ }
• SetLike.mk_smul_of_tower_mk 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) (r : M) (x : α) (hx : x ∈ s) : r • ⟨x, hx⟩ = ⟨r • x, ⋯⟩
• SubMulAction.smul'.eq_1 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) : p.smul' = { smul := fun c x => ⟨c • ↑x, ⋯⟩ }
• SubMulAction.val_smul_of_tower 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [SMul S R] [SMul S M] [IsScalarTower S R M] (p : SubMulAction R M) (s : S) (x : ↥p) : ↑(s • x) = s • ↑x
• SetLike.smul_of_tower_def 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) (r : M) (x : ↥s) : r • x = ⟨r • ↑x, ⋯⟩
• SetLike.smul'.congr_simp 📋 Mathlib.Algebra.Module.Submodule.Defs
  {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [SetLike S α] [SMul M N] [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] (s : S) : SetLike.smul' s = SetLike.smul' s
• Submodule.smul_of_tower_mem 📋 Mathlib.Algebra.Module.Submodule.Defs
  {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (h : x ∈ p) : r • x ∈ p
• SubMulAction.mulAction'.congr_simp 📋 Mathlib.Algebra.Module.Submodule.Defs
  {S : Type u'} {R : Type u} {M : Type v} [Monoid R] [MulAction R M] [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M] (p : SubMulAction R M) : p.mulAction' = p.mulAction'
• Submodule.smul_mem_iff' 📋 Mathlib.Algebra.Module.Submodule.Defs
  {G : Type u''} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} [Group G] [MulAction G M] [SMul G R] [IsScalarTower G R M] (g : G) : g • x ∈ p ↔ x ∈ p
• Submodule.isScalarTower' 📋 Mathlib.Algebra.Module.Submodule.Defs
  {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {S' : Type u_1} [SMul S R] [SMul S M] [SMul S' R] [SMul S' M] [SMul S S'] [IsScalarTower S' R M] [IsScalarTower S S' M] [IsScalarTower S R M] : IsScalarTower S S' ↥p
• Submodule.isScalarTower 📋 Mathlib.Algebra.Module.Submodule.Defs
  {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] : IsScalarTower S R ↥p
• Submodule.coe_smul_of_tower 📋 Mathlib.Algebra.Module.Submodule.Defs
  {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : ↥p) : ↑(r • x) = r • ↑x
• Submodule.isCentralScalar 📋 Mathlib.Algebra.Module.Submodule.Basic
  {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S ↥p
• Submodule.smul_mem_iff 📋 Mathlib.Algebra.Module.Submodule.Basic
  {S : Type u'} {R : Type u} {M : Type v} [DivisionSemiring S] [Semiring R] [AddCommMonoid M] [Module R M] [SMul S R] [Module S M] [IsScalarTower S R M] (p : Submodule R M) {s : S} {x : M} (s0 : s ≠ 0) : s • x ∈ p ↔ x ∈ p
• Submodule.restrictScalars_injective 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] : Function.Injective (Submodule.restrictScalars S)
• Submodule.toAddSubmonoid_restrictScalars 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) : (Submodule.restrictScalars S V).toAddSubmonoid = V.toAddSubmonoid
• Submodule.restrictScalars_bot 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] : Submodule.restrictScalars S ⊥ = ⊥
• Submodule.restrictScalars_top 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] : Submodule.restrictScalars S ⊤ = ⊤
• Submodule.coe_restrictScalars 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) : ↑(Submodule.restrictScalars S V) = ↑V
• Submodule.restrictScalars.congr_simp 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V V✝ : Submodule R M) (e_V : V = V✝) : Submodule.restrictScalars S V = Submodule.restrictScalars S V✝
• Submodule.restrictScalars_inj 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] {V₁ V₂ : Submodule R M} : Submodule.restrictScalars S V₁ = Submodule.restrictScalars S V₂ ↔ V₁ = V₂
• Submodule.restrictScalars_eq_bot_iff 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] {p : Submodule R M} : Submodule.restrictScalars S p = ⊥ ↔ p = ⊥
• Submodule.restrictScalars_eq_top_iff 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] {p : Submodule R M} : Submodule.restrictScalars S p = ⊤ ↔ p = ⊤
• Submodule.restrictScalars_mem 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) (m : M) : m ∈ Submodule.restrictScalars S V ↔ m ∈ V
• Submodule.restrictScalarsEmbedding_apply 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (V : Submodule R M) : (Submodule.restrictScalarsEmbedding S R M) V = Submodule.restrictScalars S V
• Submodule.restrictScalarsEquiv_apply 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) (a✝ : ↥p) : (Submodule.restrictScalarsEquiv S R M p) a✝ = a✝
• Submodule.restrictScalars.isScalarTower 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) : IsScalarTower S R ↥(Submodule.restrictScalars S p)
• Submodule.restrictScalarsEquiv_symm_apply 📋 Mathlib.Algebra.Module.Submodule.RestrictScalars
  (S : Type u_1) (R : Type u_2) (M : Type u_3) [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] (p : Submodule R M) (a✝ : ↥p) : (Submodule.restrictScalarsEquiv S R M p).symm a✝ = a✝
• ULift.isScalarTower 📋 Mathlib.Algebra.Module.ULift
  {R : Type u} {M : Type v} {N : Type w} [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] : IsScalarTower (ULift.{u_1, u} R) M N
• ULift.isScalarTower' 📋 Mathlib.Algebra.Module.ULift
  {R : Type u} {M : Type v} {N : Type w} [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] : IsScalarTower R (ULift.{u_1, v} M) N
• ULift.isScalarTower'' 📋 Mathlib.Algebra.Module.ULift
  {R : Type u} {M : Type v} {N : Type w} [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] : IsScalarTower R M (ULift.{u_1, w} N)
• Subsemiring.isScalarTower 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R' : Type u_1} {α : Type u_2} {β : Type u_3} [NonAssocSemiring R'] [SMul α β] [SMul R' α] [SMul R' β] [IsScalarTower R' α β] (S : Subsemiring R') : IsScalarTower (↥S) α β
• Subring.instIsScalarTowerSubtypeMem 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} [Ring R] {α : Type u_1} {β : Type u_2} [SMul α β] [SMul R α] [SMul R β] [IsScalarTower R α β] (S : Subring R) : IsScalarTower (↥S) α β
• IsScalarTower.to_smulCommClass 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : SMulCommClass R A M
• IsScalarTower.to_smulCommClass' 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : SMulCommClass A R M
• Module.End.instAlgebra.congr_simp 📋 Mathlib.Algebra.Algebra.Basic
  (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] : Module.End.instAlgebra R S M = Module.End.instAlgebra R S M
• NoZeroSMulDivisors.trans_faithfulSMul 📋 Mathlib.Algebra.Algebra.Basic
  (R : Type u_4) (A : Type u_5) (M : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [FaithfulSMul R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors A M] : NoZeroSMulDivisors R M
• algebraMap_smul 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u_1} [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (r : R) (m : M) : (algebraMap R A) r • m = r • m
• algebra_compatible_smul 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u_1} [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (r : R) (m : M) : r • m = (algebraMap R A) r • m
• NeZero.of_faithfulSMul 📋 Mathlib.Algebra.Algebra.Basic
  (R : Type u_1) (A : Type u_2) [Semiring R] [Semiring A] [Module R A] [IsScalarTower R A A] [FaithfulSMul R A] (n : ℕ) [NeZero ↑n] : NeZero ↑n
• smul_algebra_smul_comm 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (r : R) (a : A) (m : M) : a • r • m = r • a • m
• Module.algebraMap_end_apply 📋 Mathlib.Algebra.Algebra.Basic
  (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] (a : R) (m : M) : ((algebraMap R (Module.End S M)) a) m = a • m
• LinearMap.ker_restrictScalars 📋 Mathlib.Algebra.Algebra.Basic
  (R : Type u_1) {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [SMul R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[S] N) : (↑R f).ker = Submodule.restrictScalars R f.ker
• Module.algebraMap_end_eq_smul_id 📋 Mathlib.Algebra.Algebra.Basic
  (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] (a : R) : (algebraMap R (Module.End S M)) a = a • LinearMap.id
• LinearMap.extendScalarsOfSurjective_apply 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u_1} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S M] [IsScalarTower R S M] [Module R N] [Module S N] [IsScalarTower R S N] (h : Function.Surjective ⇑(algebraMap R S)) (l : M →ₗ[R] N) (x : M) : (LinearMap.extendScalarsOfSurjective h l) x = l x
• LinearEquiv.extendScalarsOfSurjective_symm 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u_1} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S M] [IsScalarTower R S M] [Module R N] [Module S N] [IsScalarTower R S N] (h : Function.Surjective ⇑(algebraMap R S)) (f : M ≃ₗ[R] N) : (LinearEquiv.extendScalarsOfSurjective h f).symm = LinearEquiv.extendScalarsOfSurjective h f.symm
• Module.End.algebraMap_isUnit_inv_apply_eq_iff 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u} (S : Type v) {M : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] {x : R} (h : IsUnit ((algebraMap R (Module.End S M)) x)) (m m' : M) : ↑h.unit⁻¹ m = m' ↔ m = x • m'
• Module.End.algebraMap_isUnit_inv_apply_eq_iff' 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u} (S : Type v) {M : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] {x : R} (h : IsUnit ((algebraMap R (Module.End S M)) x)) (m m' : M) : m' = ↑h.unit⁻¹ m ↔ m = x • m'
• LinearEquiv.extendScalarsOfSurjective_apply 📋 Mathlib.Algebra.Algebra.Basic
  {R : Type u_1} {S : Type u_4} [CommSemiring R] [Semiring S] [Algebra R S] {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S M] [IsScalarTower R S M] [Module R N] [Module S N] [IsScalarTower R S N] (h : Function.Surjective ⇑(algebraMap R S)) (f : M ≃ₗ[R] N) (x : M) : (LinearEquiv.extendScalarsOfSurjective h f) x = f x
• AlgEquiv.apply_smulCommClass 📋 Mathlib.Algebra.Algebra.Equiv
  {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] {S : Type u_1} [SMul S R] [SMul S A₁] [IsScalarTower S R A₁] : SMulCommClass S (A₁ ≃ₐ[R] A₁) A₁
• AlgEquiv.apply_smulCommClass' 📋 Mathlib.Algebra.Algebra.Equiv
  {R : Type uR} {A₁ : Type uA₁} [CommSemiring R] [Semiring A₁] [Algebra R A₁] {S : Type u_1} [SMul S R] [SMul S A₁] [IsScalarTower S R A₁] : SMulCommClass (A₁ ≃ₐ[R] A₁) S A₁
• LinearMap.mulLeftRight.congr_simp 📋 Mathlib.Algebra.Algebra.Equiv
  (R : Type u_14) {A : Type u_15} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (ab ab✝ : A × A) (e_ab : ab = ab✝) : LinearMap.mulLeftRight R ab = LinearMap.mulLeftRight R ab✝
• LinearEquiv.symm_conjAlgEquiv 📋 Mathlib.Algebra.Algebra.Equiv
  {R : Type u_1} {S : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [Semiring S] [Module S M₁] [Module S M₂] [SMulCommClass S R M₁] [SMulCommClass S R M₂] [SMul R S] [IsScalarTower R S M₁] [IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂) : (LinearEquiv.conjAlgEquiv R e).symm = LinearEquiv.conjAlgEquiv R e.symm
• LinearEquiv.conjAlgEquiv_apply 📋 Mathlib.Algebra.Algebra.Equiv
  {R : Type u_1} {S : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [Semiring S] [Module S M₁] [Module S M₂] [SMulCommClass S R M₁] [SMulCommClass S R M₂] [SMul R S] [IsScalarTower R S M₁] [IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂) (f : Module.End S M₁) : (LinearEquiv.conjAlgEquiv R e) f = ↑e ∘ₗ f ∘ₗ ↑e.symm
• LinearEquiv.conjAlgEquiv_apply_apply 📋 Mathlib.Algebra.Algebra.Equiv
  (R : Type u_1) {S : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [Semiring S] [Module S M₁] [Module S M₂] [SMulCommClass S R M₁] [SMulCommClass S R M₂] [SMul R S] [IsScalarTower R S M₁] [IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂) (f : M₁ →ₗ[S] M₁) (a✝ : M₂) : ((LinearEquiv.conjAlgEquiv R e) f) a✝ = e (f (e.symm a✝))
• LinearEquiv.conjAlgEquiv_symm_apply_apply 📋 Mathlib.Algebra.Algebra.Equiv
  (R : Type u_1) {S : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [Semiring S] [Module S M₁] [Module S M₂] [SMulCommClass S R M₁] [SMulCommClass S R M₂] [SMul R S] [IsScalarTower R S M₁] [IsScalarTower R S M₂] (e : M₁ ≃ₗ[S] M₂) (f : M₂ →ₗ[S] M₂) (a✝ : M₁) : ((LinearEquiv.conjAlgEquiv R e).symm f) a✝ = e.symm (f (e a✝))
• LinearMap.range_restrictScalars 📋 Mathlib.Algebra.Module.Submodule.Range
  {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] [SMul R R₂] [Module R₂ M] [Module R M₂] [LinearMap.CompatibleSMul M M₂ R R₂] [IsScalarTower R R₂ M₂] (f : M →ₗ[R₂] M₂) : (↑R f).range = Submodule.restrictScalars R f.range
• Submodule.restrictScalars_map 📋 Mathlib.Algebra.Module.Submodule.Range
  {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] [SMul R R₂] [Module R₂ M] [Module R M₂] [IsScalarTower R R₂ M] [IsScalarTower R R₂ M₂] (f : M →ₗ[R₂] M₂) (M' : Submodule R₂ M) : Submodule.restrictScalars R (Submodule.map f M') = Submodule.map (↑R f) (Submodule.restrictScalars R M')
• Submodule.span_singleton_smul_le 📋 Mathlib.LinearAlgebra.Span.Defs
  (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_9} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : M) : R ∙ r • x ≤ R ∙ x
• Submodule.span_singleton_group_smul_eq 📋 Mathlib.LinearAlgebra.Span.Defs
  (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_9} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] (g : G) (x : M) : R ∙ g • x = R ∙ x
• Submodule.span_span_of_tower 📋 Mathlib.LinearAlgebra.Span.Basic
  (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] : Submodule.span S ↑(Submodule.span R s) = Submodule.span S s
• Submodule.span_coe_eq_restrictScalars 📋 Mathlib.LinearAlgebra.Span.Basic
  {R : Type u_1} {M : Type u_4} {S : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : Submodule.span S ↑p = Submodule.restrictScalars S p
• Submodule.span_subset_span 📋 Mathlib.LinearAlgebra.Span.Basic
  (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] : ↑(Submodule.span R s) ⊆ ↑(Submodule.span S s)
• Submodule.span_eq_top_of_span_eq_top 📋 Mathlib.LinearAlgebra.Span.Basic
  (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] (s : Set M) (hs : Submodule.span R s = ⊤) : Submodule.span S s = ⊤
• Submodule.span_le_restrictScalars 📋 Mathlib.LinearAlgebra.Span.Basic
  (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] : Submodule.span R s ≤ Submodule.restrictScalars R (Submodule.span S s)
• Submodule.module'.congr_simp 📋 Mathlib.LinearAlgebra.Span.Basic
  {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : p.module' = p.module'
• Submodule.injective_inclusionSpan 📋 Mathlib.LinearAlgebra.Span.Basic
  {R : Type u_1} {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] (p : Submodule R M) : Function.Injective ⇑(Submodule.inclusionSpan S p)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 6ff4759 serving mathlib revision abad10c