chore: mathlib4-ify names (#2557)

`is_scalar_tower` is now `IsScalarTower` etc. As discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/naming.20conventions/near/338862658), this also renames `sMulCommClass` to `smulCommClass`. The later was already the majority spelling.
leanprover-community · Mar 2, 2023 · fc37ee9 · fc37ee9
1 parent a8ede0d
commit fc37ee9
Show file tree

Hide file tree

Showing 13 changed files with 43 additions and 43 deletions.
diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean
@@ -902,16 +902,16 @@ theorem NoZeroSMulDivisors.trans (R A M : Type _) [CommRing R] [Ring A] [IsDomai
 variable {A}
 
 -- see Note [lower instance priority]
-instance (priority := 100) IsScalarTower.to_sMulCommClass : SMulCommClass R A M :=
+instance (priority := 100) IsScalarTower.to_smulCommClass : SMulCommClass R A M :=
   ⟨fun r a m => by
     rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ←
       algebra_compatible_smul]⟩
-#align is_scalar_tower.to_smul_comm_class IsScalarTower.to_sMulCommClass
+#align is_scalar_tower.to_smul_comm_class IsScalarTower.to_smulCommClass
 
 -- see Note [lower instance priority]
-instance (priority := 100) IsScalarTower.to_sMulCommClass' : SMulCommClass A R M :=
+instance (priority := 100) IsScalarTower.to_smulCommClass' : SMulCommClass A R M :=
   SMulCommClass.symm _ _ _
-#align is_scalar_tower.to_smul_comm_class' IsScalarTower.to_sMulCommClass'
+#align is_scalar_tower.to_smul_comm_class' IsScalarTower.to_smulCommClass'
 
 theorem smul_algebra_smul_comm (r : R) (a : A) (m : M) : a • r • m = r • a • m :=
   smul_comm _ _ _

diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean
@@ -727,13 +727,13 @@ instance apply_faithfulSMul : FaithfulSMul (A₁ ≃ₐ[R] A₁) A₁ :=
   ⟨AlgEquiv.ext⟩
 #align alg_equiv.apply_has_faithful_smul AlgEquiv.apply_faithfulSMul
 
-instance apply_sMulCommClass : SMulCommClass R (A₁ ≃ₐ[R] A₁) A₁
+instance apply_smulCommClass : SMulCommClass R (A₁ ≃ₐ[R] A₁) A₁
     where smul_comm r e a := (e.map_smul r a).symm
-#align alg_equiv.apply_smul_comm_class AlgEquiv.apply_sMulCommClass
+#align alg_equiv.apply_smul_comm_class AlgEquiv.apply_smulCommClass
 
-instance apply_smul_comm_class' : SMulCommClass (A₁ ≃ₐ[R] A₁) R A₁
+instance apply_smulCommClass' : SMulCommClass (A₁ ≃ₐ[R] A₁) R A₁
     where smul_comm e r a := e.map_smul r a
-#align alg_equiv.apply_smul_comm_class' AlgEquiv.apply_smul_comm_class'
+#align alg_equiv.apply_smul_comm_class' AlgEquiv.apply_smulCommClass'
 
 @[simp]
 theorem algebraMap_eq_apply (e : A₁ ≃ₐ[R] A₂) {y : R} {x : A₁} :

diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean
@@ -413,11 +413,11 @@ def AddCommMonoid.natModule.unique : Unique (Module ℕ M) where
   uniq P := (Module.ext' P _) fun n => by convert nat_smul_eq_nsmul P n
 #align add_comm_monoid.nat_module.unique AddCommMonoid.natModule.unique
 
-instance AddCommMonoid.nat_is_scalar_tower : IsScalarTower ℕ R M where
+instance AddCommMonoid.nat_isScalarTower : IsScalarTower ℕ R M where
   smul_assoc n x y :=
     Nat.recOn n (by simp only [Nat.zero_eq, zero_smul])
     fun n ih => by simp only [Nat.succ_eq_add_one, add_smul, one_smul, ih]
-#align add_comm_monoid.nat_is_scalar_tower AddCommMonoid.nat_is_scalar_tower
+#align add_comm_monoid.nat_is_scalar_tower AddCommMonoid.nat_isScalarTower
 
 end AddCommMonoid
 

diff --git a/Mathlib/Algebra/Module/Submodule/Basic.lean b/Mathlib/Algebra/Module/Submodule/Basic.lean
@@ -279,10 +279,10 @@ instance [SMul S R] [SMul S M] [IsScalarTower S R M] : SMul S p :=
 instance [SMul S R] [SMul S M] [IsScalarTower S R M] : IsScalarTower S R p :=
   p.toSubMulAction.isScalarTower
 
-instance is_scalar_tower' {S' : Type _} [SMul S R] [SMul S M] [SMul S' R] [SMul S' M] [SMul S S']
+instance isScalarTower' {S' : Type _} [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 :=
   p.toSubMulAction.isScalarTower'
-#align submodule.is_scalar_tower' Submodule.is_scalar_tower'
+#align submodule.is_scalar_tower' Submodule.isScalarTower'
 
 instance [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 :=

diff --git a/Mathlib/Data/Real/ENNReal.lean b/Mathlib/Data/Real/ENNReal.lean
@@ -457,13 +457,13 @@ theorem smul_def {M : Type _} [MulAction ℝ≥0∞ M] (c : ℝ≥0) (x : M) : c
 instance {M N : Type _} [MulAction ℝ≥0∞ M] [MulAction ℝ≥0∞ N] [SMul M N] [IsScalarTower ℝ≥0∞ M N] :
     IsScalarTower ℝ≥0 M N where smul_assoc r := (smul_assoc (r : ℝ≥0∞) : _)
 
-instance sMulCommClass_left {M N : Type _} [MulAction ℝ≥0∞ N] [SMul M N] [SMulCommClass ℝ≥0∞ M N] :
+instance smulCommClass_left {M N : Type _} [MulAction ℝ≥0∞ N] [SMul M N] [SMulCommClass ℝ≥0∞ M N] :
     SMulCommClass ℝ≥0 M N where smul_comm r := (smul_comm (r : ℝ≥0∞) : _)
-#align ennreal.smul_comm_class_left ENNReal.sMulCommClass_left
+#align ennreal.smul_comm_class_left ENNReal.smulCommClass_left
 
-instance sMulCommClass_right {M N : Type _} [MulAction ℝ≥0∞ N] [SMul M N] [SMulCommClass M ℝ≥0∞ N] :
+instance smulCommClass_right {M N : Type _} [MulAction ℝ≥0∞ N] [SMul M N] [SMulCommClass M ℝ≥0∞ N] :
     SMulCommClass M ℝ≥0 N where smul_comm m r := (smul_comm m (r : ℝ≥0∞) : _)
-#align ennreal.smul_comm_class_right ENNReal.sMulCommClass_right
+#align ennreal.smul_comm_class_right ENNReal.smulCommClass_right
 
 /-- A `DistribMulAction` over `ℝ≥0∞` restricts to a `DistribMulAction` over `ℝ≥0`. -/
 noncomputable instance {M : Type _} [AddMonoid M] [DistribMulAction ℝ≥0∞ M] :

diff --git a/Mathlib/Data/Real/NNReal.lean b/Mathlib/Data/Real/NNReal.lean
@@ -252,13 +252,13 @@ theorem smul_def {M : Type _} [MulAction ℝ M] (c : ℝ≥0) (x : M) : c • x
 instance {M N : Type _} [MulAction ℝ M] [MulAction ℝ N] [SMul M N] [IsScalarTower ℝ M N] :
     IsScalarTower ℝ≥0 M N where smul_assoc r := (smul_assoc (r : ℝ) : _)
 
-instance sMulCommClass_left {M N : Type _} [MulAction ℝ N] [SMul M N] [SMulCommClass ℝ M N] :
+instance smulCommClass_left {M N : Type _} [MulAction ℝ N] [SMul M N] [SMulCommClass ℝ M N] :
     SMulCommClass ℝ≥0 M N where smul_comm r := (smul_comm (r : ℝ) : _)
-#align nnreal.smul_comm_class_left NNReal.sMulCommClass_left
+#align nnreal.smul_comm_class_left NNReal.smulCommClass_left
 
-instance sMulCommClass_right {M N : Type _} [MulAction ℝ N] [SMul M N] [SMulCommClass M ℝ N] :
+instance smulCommClass_right {M N : Type _} [MulAction ℝ N] [SMul M N] [SMulCommClass M ℝ N] :
     SMulCommClass M ℝ≥0 N where smul_comm m r := (smul_comm m (r : ℝ) : _)
-#align nnreal.smul_comm_class_right NNReal.sMulCommClass_right
+#align nnreal.smul_comm_class_right NNReal.smulCommClass_right
 
 /-- A `DistribMulAction` over `ℝ` restricts to a `DistribMulAction` over `ℝ≥0`. -/
 instance {M : Type _} [AddMonoid M] [DistribMulAction ℝ M] : DistribMulAction ℝ≥0 M :=

diff --git a/Mathlib/GroupTheory/MonoidLocalization.lean b/Mathlib/GroupTheory/MonoidLocalization.lean
@@ -437,7 +437,7 @@ protected def smul [SMul R M] [IsScalarTower R M M] (c : R) (z : Localization S)
         cases' h with t ht
         use t
         dsimp only [Subtype.coe_mk] at ht ⊢
--- TODO: this definition should take `smul_comm_class R M M` instead of `is_scalar_tower R M M` if
+-- TODO: this definition should take `SMulCommClass R M M` instead of `IsScalarTower R M M` if
 -- we ever want to generalize to the non-commutative case.
         haveI : SMulCommClass R M M :=
           ⟨fun r m₁ m₂ ↦ by simp_rw [smul_eq_mul, mul_comm m₁, smul_mul_assoc]⟩
@@ -461,15 +461,15 @@ instance [SMul R₁ M] [SMul R₂ M] [IsScalarTower R₁ M M] [IsScalarTower R
   [IsScalarTower R₁ R₂ M] : IsScalarTower R₁ R₂ (Localization S) where
   smul_assoc s t := Localization.ind <| Prod.rec fun r x ↦ by simp only [smul_mk, smul_assoc s t r]
 
-instance sMulCommClass_right {R : Type _} [SMul R M] [IsScalarTower R M M] :
+instance smulCommClass_right {R : Type _} [SMul R M] [IsScalarTower R M M] :
   SMulCommClass R (Localization S) (Localization S) where
   smul_comm s :=
       Localization.ind <|
         Prod.rec fun r₁ x₁ ↦
           Localization.ind <|
             Prod.rec fun r₂ x₂ ↦ by
               simp only [smul_mk, smul_eq_mul, mk_mul, mul_comm r₁, smul_mul_assoc]
-#align localization.smul_comm_class_right Localization.sMulCommClass_right
+#align localization.smul_comm_class_right Localization.smulCommClass_right
 
 instance isScalarTower_right {R : Type _} [SMul R M] [IsScalarTower R M M] :
   IsScalarTower R (Localization S) (Localization S) where

diff --git a/Mathlib/LinearAlgebra/Quotient.lean b/Mathlib/LinearAlgebra/Quotient.lean
@@ -146,10 +146,10 @@ theorem mk_smul (r : S) (x : M) : (mk (r • x) : M ⧸ p) = r • mk x :=
   rfl
 #align submodule.quotient.mk_smul Submodule.Quotient.mk_smul
 
-instance sMulCommClass (T : Type _) [SMul T R] [SMul T M] [IsScalarTower T R M]
+instance smulCommClass (T : Type _) [SMul T R] [SMul T M] [IsScalarTower T R M]
     [SMulCommClass S T M] : SMulCommClass S T (M ⧸ P)
     where smul_comm _x _y := Quotient.ind' fun _z => congr_arg mk (smul_comm _ _ _)
-#align submodule.quotient.smul_comm_class Submodule.Quotient.sMulCommClass
+#align submodule.quotient.smul_comm_class Submodule.Quotient.smulCommClass
 
 instance isScalarTower (T : Type _) [SMul T R] [SMul T M] [IsScalarTower T R M] [SMul S T]
     [IsScalarTower S T M] : IsScalarTower S T (M ⧸ P)

diff --git a/Mathlib/LinearAlgebra/TensorProduct.lean b/Mathlib/LinearAlgebra/TensorProduct.lean
@@ -177,7 +177,7 @@ class CompatibleSMul [DistribMulAction R' N] where
 end
 
 /-- Note that this provides the default `compatible_smul R R M N` instance through
-`mul_action.is_scalar_tower.left`. -/
+`IsScalarTower.left`. -/
 instance (priority := 100) CompatibleSMul.isScalarTower [SMul R' R] [IsScalarTower R' R M]
     [DistribMulAction R' N] [IsScalarTower R' R N] : CompatibleSMul R R' M N :=
   ⟨fun r m n => by

diff --git a/Mathlib/Order/Filter/Germ.lean b/Mathlib/Order/Filter/Germ.lean
@@ -382,11 +382,11 @@ instance rightCancelSemigroup [RightCancelSemigroup M] : RightCancelSemigroup (G
       inductionOn₃ f₁ f₂ f₃ fun _f₁ _f₂ _f₃ H =>
         coe_eq.2 <| (coe_eq.1 H).mono fun _x => mul_right_cancel }
 
-@[to_additive vAdd]
-instance sMul [SMul M G] : SMul M (Germ l G) :=
+@[to_additive]
+instance smul [SMul M G] : SMul M (Germ l G) :=
   ⟨fun n => map (n • ·)⟩
 
-@[to_additive existing sMul]
+@[to_additive existing smul]
 instance pow [Pow G M] : Pow (Germ l G) M :=
   ⟨fun f n => map (· ^ n) f⟩
 

diff --git a/Mathlib/Order/Filter/Pointwise.lean b/Mathlib/Order/Filter/Pointwise.lean
@@ -1288,19 +1288,19 @@ instance isScalarTower [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α
 #align filter.vadd_assoc_class Filter.vaddAssocClass
 
 @[to_additive vaddAssocClass']
-instance is_scalar_tower' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
+instance isScalarTower' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
     IsScalarTower α (Filter β) (Filter γ) :=
   ⟨fun a f g => by
     refine' (map_map₂_distrib_left fun _ _ => _).symm
     exact (smul_assoc a _ _).symm⟩
-#align filter.is_scalar_tower' Filter.is_scalar_tower'
+#align filter.is_scalar_tower' Filter.isScalarTower'
 #align filter.vadd_assoc_class' Filter.vaddAssocClass'
 
 @[to_additive vaddAssocClass'']
-instance is_scalar_tower'' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
+instance isScalarTower'' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] :
     IsScalarTower (Filter α) (Filter β) (Filter γ) :=
   ⟨fun _ _ _ => map₂_assoc smul_assoc⟩
-#align filter.is_scalar_tower'' Filter.is_scalar_tower''
+#align filter.is_scalar_tower'' Filter.isScalarTower''
 #align filter.vadd_assoc_class'' Filter.vaddAssocClass''
 
 @[to_additive]

diff --git a/Mathlib/RingTheory/Subring/Basic.lean b/Mathlib/RingTheory/Subring/Basic.lean
@@ -1446,14 +1446,14 @@ instance [Semiring α] [MulSemiringAction R α] (S : Subring R) : MulSemiringAct
   inferInstanceAs (MulSemiringAction S.toSubmonoid α)
 
 /-- The center of a semiring acts commutatively on that semiring. -/
-instance center.sMulCommClass_left : SMulCommClass (center R) R R :=
-  Subsemiring.center.sMulCommClass_left
-#align subring.center.smul_comm_class_left Subring.center.sMulCommClass_left
+instance center.smulCommClass_left : SMulCommClass (center R) R R :=
+  Subsemiring.center.smulCommClass_left
+#align subring.center.smul_comm_class_left Subring.center.smulCommClass_left
 
 /-- The center of a semiring acts commutatively on that semiring. -/
-instance center.sMulCommClass_right : SMulCommClass R (center R) R :=
-  Subsemiring.center.sMulCommClass_right
-#align subring.center.smul_comm_class_right Subring.center.sMulCommClass_right
+instance center.smulCommClass_right : SMulCommClass R (center R) R :=
+  Subsemiring.center.smulCommClass_right
+#align subring.center.smul_comm_class_right Subring.center.smulCommClass_right
 
 end Subring
 

diff --git a/Mathlib/RingTheory/Subsemiring/Basic.lean b/Mathlib/RingTheory/Subsemiring/Basic.lean
@@ -1387,14 +1387,14 @@ instance [Semiring α] [MulSemiringAction R' α] (S : Subsemiring R') : MulSemir
   S.toSubmonoid.mulSemiringAction
 
 /-- The center of a semiring acts commutatively on that semiring. -/
-instance center.sMulCommClass_left : SMulCommClass (center R') R' R' :=
+instance center.smulCommClass_left : SMulCommClass (center R') R' R' :=
   Submonoid.center.smulCommClass_left
-#align subsemiring.center.smul_comm_class_left Subsemiring.center.sMulCommClass_left
+#align subsemiring.center.smul_comm_class_left Subsemiring.center.smulCommClass_left
 
 /-- The center of a semiring acts commutatively on that semiring. -/
-instance center.sMulCommClass_right : SMulCommClass R' (center R') R' :=
+instance center.smulCommClass_right : SMulCommClass R' (center R') R' :=
   Submonoid.center.smulCommClass_right
-#align subsemiring.center.smul_comm_class_right Subsemiring.center.sMulCommClass_right
+#align subsemiring.center.smul_comm_class_right Subsemiring.center.smulCommClass_right
 
 /-- If all the elements of a set `s` commute, then `closure s` is a commutative monoid. -/
 def closureCommSemiringOfComm {s : Set R'} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) :