chore(Algebra): rename theorems for consistency (#20271)

artie2000 · artie2000 · commit e8a30842b99b · 2024-12-28T03:20:01.000Z
Taking chore material out of #16094 to make the diff cleaner. Moves: isSquare_one -> IsSquare.one isSquare_sq -> IsSquare.sq even_two_nsmul -> Even.two_nsmul isSumSq_sum_mul_self -> IsSumSq.mul_self
diff --git a/Mathlib/Algebra/Group/Even.lean b/Mathlib/Algebra/Group/Even.lean
@@ -88,7 +88,9 @@ instance Multiplicative.instDecidablePredIsSquare [DecidablePred (Even : α →
 end Add
 
 @[to_additive (attr := simp)]
-lemma isSquare_one [MulOneClass α] : IsSquare (1 : α) := ⟨1, (mul_one _).symm⟩
+lemma IsSquare.one [MulOneClass α] : IsSquare (1 : α) := ⟨1, (mul_one _).symm⟩
+
+@[to_additive, deprecated (since := "2024-12-27")] alias isSquare_one := IsSquare.one
 
 @[to_additive]
 lemma IsSquare.map [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β]
@@ -114,7 +116,10 @@ attribute [to_additive Even.exists_two_nsmul
 @[to_additive Even.nsmul'] lemma Even.isSquare_pow : Even n → ∀ a : α, IsSquare (a ^ n) := by
   rintro ⟨n, rfl⟩ a; exact ⟨a ^ n, pow_add _ _ _⟩
 
-@[to_additive even_two_nsmul] lemma IsSquare_sq (a : α) : IsSquare (a ^ 2) := ⟨a, pow_two _⟩
+@[to_additive Even.two_nsmul] lemma IsSquare.sq (a : α) : IsSquare (a ^ 2) := ⟨a, pow_two _⟩
+
+@[deprecated (since := "2024-12-27")] alias IsSquare_sq := IsSquare.sq
+@[deprecated (since := "2024-12-27")] alias even_two_nsmul := Even.two_nsmul
 
 end Monoid
 
diff --git a/Mathlib/Algebra/Ring/SumsOfSquares.lean b/Mathlib/Algebra/Ring/SumsOfSquares.lean
@@ -61,14 +61,16 @@ theorem IsSumSq.add [AddMonoid R] {S1 S2 : R} (p1 : IsSumSq S1)
 @[deprecated (since := "2024-08-09")] alias isSumSq.add := IsSumSq.add
 
 /-- A finite sum of squares is a sum of squares. -/
-theorem isSumSq_sum_mul_self {ι : Type*} [AddCommMonoid R] (s : Finset ι) (f : ι → R) :
+theorem IsSumSq.sum_mul_self {ι : Type*} [AddCommMonoid R] (s : Finset ι) (f : ι → R) :
     IsSumSq (∑ i ∈ s, f i * f i) := by
   induction s using Finset.cons_induction with
   | empty =>
     simpa only [Finset.sum_empty] using IsSumSq.zero
   | cons i s his h =>
     exact (Finset.sum_cons (β := R) his) ▸ IsSumSq.sq_add (f i) (∑ i ∈ s, f i * f i) h
 
+@[deprecated (since := "2024-12-27")] alias isSumSq_sum_mul_self := IsSumSq.sum_mul_self
+
 variable (R) in
 /--
 In an additive monoid with multiplication `R`, the type `sumSqIn R` is the submonoid of sums of
diff --git a/Mathlib/Data/Rat/Lemmas.lean b/Mathlib/Data/Rat/Lemmas.lean
@@ -119,11 +119,11 @@ theorem isSquare_iff {q : ℚ} : IsSquare q ↔ IsSquare q.num ∧ IsSquare q.de
 
 @[norm_cast, simp]
 theorem isSquare_natCast_iff {n : ℕ} : IsSquare (n : ℚ) ↔ IsSquare n := by
-  simp_rw [isSquare_iff, num_natCast, den_natCast, isSquare_one, and_true, Int.isSquare_natCast_iff]
+  simp_rw [isSquare_iff, num_natCast, den_natCast, IsSquare.one, and_true, Int.isSquare_natCast_iff]
 
 @[norm_cast, simp]
 theorem isSquare_intCast_iff {z : ℤ} : IsSquare (z : ℚ) ↔ IsSquare z := by
-  simp_rw [isSquare_iff, intCast_num, intCast_den, isSquare_one, and_true]
+  simp_rw [isSquare_iff, intCast_num, intCast_den, IsSquare.one, and_true]
 
 -- See note [no_index around OfNat.ofNat]
 @[simp]
diff --git a/Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean b/Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
@@ -189,7 +189,7 @@ lemma corootForm_self_smul_root (i : ι) :
 
 lemma rootForm_self_sum_of_squares (x : M) :
     IsSumSq (P.RootForm x x) :=
-  P.rootForm_apply_apply x x ▸ isSumSq_sum_mul_self Finset.univ _
+  P.rootForm_apply_apply x x ▸ IsSumSq.sum_mul_self Finset.univ _
 
 lemma rootForm_root_self (j : ι) :
     P.RootForm (P.root j) (P.root j) = ∑ (i : ι), (P.pairing j i) * (P.pairing j i) := by
diff --git a/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean b/Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
@@ -73,7 +73,7 @@ theorem quadraticCharFun_zero : quadraticCharFun F 0 = 0 := by
 
 @[simp]
 theorem quadraticCharFun_one : quadraticCharFun F 1 = 1 := by
-  simp only [quadraticCharFun, one_ne_zero, isSquare_one, if_true, if_false]
+  simp only [quadraticCharFun, one_ne_zero, IsSquare.one, if_true, if_false]
 
 /-- If `ringChar F = 2`, then `quadraticCharFun F` takes the value `1` on nonzero elements. -/
 theorem quadraticCharFun_eq_one_of_char_two (hF : ringChar F = 2) {a : F} (ha : a ≠ 0) :
@@ -140,7 +140,7 @@ theorem quadraticChar_one_iff_isSquare {a : F} (ha : a ≠ 0) :
 
 /-- The quadratic character takes the value `1` on nonzero squares. -/
 theorem quadraticChar_sq_one' {a : F} (ha : a ≠ 0) : quadraticChar F (a ^ 2) = 1 := by
-  simp only [quadraticChar_apply, quadraticCharFun, sq_eq_zero_iff, ha, IsSquare_sq, if_true,
+  simp only [quadraticChar_apply, quadraticCharFun, sq_eq_zero_iff, ha, IsSquare.sq, if_true,
     if_false]
 
 /-- The square of the quadratic character on nonzero arguments is `1`. -/
