chore: Fixed occurences of 'Smul' (#1570)

leanprover-community · Jan 14, 2023 · d2bf5c7 · d2bf5c7
1 parent dceaab4
commit d2bf5c7
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean
@@ -666,7 +666,7 @@ section AddCommGroup
 -- `R` can still be a semiring here
 variable [Semiring R] [AddCommGroup M] [Module R M]
 
-section SmulInjective
+section SMulInjective
 
 variable (M)
 
@@ -682,7 +682,7 @@ theorem smul_right_inj [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) {x y : M}
   (smul_right_injective M hc).eq_iff
 #align smul_right_inj smul_right_inj
 
-end SmulInjective
+end SMulInjective
 
 section Nat
 

diff --git a/Mathlib/Data/Rat/Cast.lean b/Mathlib/Data/Rat/Cast.lean
@@ -530,22 +530,22 @@ theorem unop_ratCast (r : ℚ) : unop (r : αᵐᵒᵖ) = r := by
 
 end MulOpposite
 
-section Smul
+section SMul
 
 namespace Rat
 
 variable {K : Type _} [DivisionRing K]
 
-instance (priority := 100) distribSmul : DistribSMul ℚ K where
+instance (priority := 100) distribSMul : DistribSMul ℚ K where
   smul := (· • ·)
   smul_zero a := by rw [smul_def, mul_zero]
   smul_add a x y := by rw [smul_def, smul_def, smul_def, mul_add]
-#align rat.distrib_smul Rat.distribSmul
+#align rat.distrib_smul Rat.distribSMul
 
 instance isScalarTower_right : IsScalarTower ℚ K K :=
   ⟨fun a x y => by simp only [smul_def, smul_eq_mul, mul_assoc]⟩
 #align rat.is_scalar_tower_right Rat.isScalarTower_right
 
 end Rat
 
-end Smul
+end SMul
diff --git a/Mathlib/Data/Set/Pointwise/SMul.lean b/Mathlib/Data/Set/Pointwise/SMul.lean
@@ -650,7 +650,7 @@ section SMulWithZero
 variable [Zero α] [Zero β] [SMulWithZero α β] {s : Set α} {t : Set β}
 
 /-!
-Note that we have neither `SmulWithZero α (Set β)` nor `SmulWithZero (Set α) (Set β)`
+Note that we have neither `SMulWithZero α (Set β)` nor `SMulWithZero (Set α) (Set β)`
 because `0 * ∅ ≠ 0`.
 -/