chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs (#20528

)

* Make documentation clearer and more concise
* Make notation consistent
* Make proofs cleaner

This PR splits off yet more chore material from #16094

Moves:
* `sumSq` -> `AddSubmonoid.sumSq`

Mathlib/Algebra/Ring/Semireal/Defs.lean

@@ -8,12 +8,11 @@ import Mathlib.Algebra.Ring.SumsOfSquares
 /-!
 # Semireal rings
 
-A semireal ring is a non-trivial commutative ring (with unit) in which `-1` is *not* a sum of
-squares. Note that `-1` does not make sense in a semiring.
+A semireal ring is a non-trivial commutative ring (with unit) in which `-1` is *not* a
+sum of squares.
 
-For instance, linearly ordered fields are semireal, because sums of squares are positive and `-1` is
-not. More generally, linearly ordered semirings in which `a ≤ b → ∃ c, a + c = b` holds, are
-semireal.
+For instance, linearly ordered rings are semireal, because sums of squares are positive and `-1` is
+not.
 
 ## Main declaration
 
@@ -29,8 +28,8 @@ variable (R : Type*)
 
 /--
 A semireal ring is a non-trivial commutative ring (with unit) in which `-1` is *not* a sum of
-squares. Note that `-1` does not make sense in a semiring. Below we define the class `IsSemireal R`
-for all additive monoid `R` equipped with a multiplication, a multiplicative unit and a negation.
+squares. We define the class `IsSemireal R`
+for all additive monoids `R` equipped with a multiplication, a multiplicative unit and a negation.
 -/
 @[mk_iff]
 class IsSemireal [AddMonoid R] [Mul R] [One R] [Neg R] : Prop where

Mathlib/Algebra/Ring/SumsOfSquares.lean

@@ -10,114 +10,111 @@ import Mathlib.Algebra.Order.Ring.Defs
 /-!
 # Sums of squares
 
-We introduce sums of squares in a type `R` endowed with an `[Add R]`, `[Zero R]` and `[Mul R]`
-instances. Sums of squares in `R` are defined by an inductive predicate `IsSumSq : R → Prop`:
-`0 : R` is a sum of squares and if `S` is a sum of squares, then for all `a : R`, `a * a + S` is a
-sum of squares in `R`.
+We introduce a predicate for sums of squares in a ring.
 
-## Main declaration
+## Main declarations
 
-- The predicate `IsSumSq : R → Prop`, defining the property of being a sum of squares in `R`.
-
-## Auxiliary declarations
-
-- The term `sumSq R` : in an additive monoid with multiplication `R`, we introduce
-`sumSq R` as the submonoid of `R` whose carrier is the subset `{S : R | IsSumSq S}`.
-
-## Theorems
-
-- `IsSumSq.add`: if `S1` and `S2` are sums of squares in `R`, then so is `S1 + S2`.
-- `IsSumSq.nonneg`: in a linearly ordered semiring `R` with an `[ExistsAddOfLE R]` instance, sums of
-squares are non-negative.
-- `mem_sumSq_of_isSquare`: a square is a sum of squares.
-- `AddSubmonoid.closure_isSquare`: the submonoid of `R` generated by the squares in `R` is the set
-of sums of squares in `R`.
+- `IsSumSq : R → Prop`: for a type `R` with addition, multiplication and a zero,
+  an inductive predicate defining the property of being a sum of squares in `R`.
+  `0 : R` is a sum of squares and if `S` is a sum of squares, then, for all `a : R`,
+  `a * a + s` is a sum of squares.
+- `AddMonoid.sumSq R`: the submonoid of sums of squares in an additive monoid `R`
+  with multiplication.
 
 -/
 
-variable {R : Type*} [Mul R]
+variable {R : Type*}
 
 /--
-In a type `R` with an addition, a zero element and a multiplication, the property of being a sum of
-squares is defined by an inductive predicate: `0 : R` is a sum of squares and if `S` is a sum of
-squares, then for all `a : R`, `a * a + S` is a sum of squares in `R`.
+The property of being a sum of squares is defined inductively by:
+`0 : R` is a sum of squares and if `s : R` is a sum of squares,
+then for all `a : R`, `a * a + s` is a sum of squares in `R`.
 -/
 @[mk_iff]
-inductive IsSumSq [Add R] [Zero R] : R → Prop
-  | zero                              : IsSumSq 0
-  | sq_add (a S : R) (pS : IsSumSq S) : IsSumSq (a * a + S)
+inductive IsSumSq [Mul R] [Add R] [Zero R] : R → Prop
+  | zero                                    : IsSumSq 0
+  | sq_add (a : R) {s : R} (hs : IsSumSq s) : IsSumSq (a * a + s)
 
 @[deprecated (since := "2024-08-09")] alias isSumSq := IsSumSq
 
 /--
-If `S1` and `S2` are sums of squares in a semiring `R`, then `S1 + S2` is a sum of squares in `R`.
+In an additive monoid with multiplication,
+if `s₁` and `s₂` are sums of squares, then `s₁ + s₂` is a sum of squares.
 -/
-theorem IsSumSq.add [AddMonoid R] {S1 S2 : R} (p1 : IsSumSq S1)
-    (p2 : IsSumSq S2) : IsSumSq (S1 + S2) := by
-  induction p1 with
-  | zero             => rw [zero_add]; exact p2
-  | sq_add a S pS ih => rw [add_assoc]; exact IsSumSq.sq_add a (S + S2) ih
+theorem IsSumSq.add [AddMonoid R] [Mul R] {s₁ s₂ : R}
+    (h₁ : IsSumSq s₁) (h₂ : IsSumSq s₂) : IsSumSq (s₁ + s₂) := by
+  induction h₁ <;> simp_all [add_assoc, sq_add]
 
 @[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) :
-    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
+namespace AddSubmonoid
+variable {T : Type*} [AddMonoid T] [Mul T] {s : T}
 
-@[deprecated (since := "2024-12-27")] alias isSumSq_sum_mul_self := IsSumSq.sum_mul_self
-
-variable (R) in
+variable (T) in
 /--
 In an additive monoid with multiplication `R`, `AddSubmonoid.sumSq R` is the submonoid of sums of
 squares in `R`.
 -/
-def sumSq [AddMonoid R] : AddSubmonoid R where
-  carrier   := {S : R | IsSumSq S}
-  zero_mem' := IsSumSq.zero
-  add_mem'  := IsSumSq.add
+@[simps]
+def sumSq [AddMonoid T] : AddSubmonoid T where
+  carrier   := {s : T | IsSumSq s}
+  zero_mem' := .zero
+  add_mem'  := .add
+
+attribute [norm_cast] coe_sumSq
 
-@[deprecated (since := "2024-08-09")] alias SumSqIn := sumSq
-@[deprecated (since := "2025-01-03")] alias sumSqIn := sumSq
+@[simp] theorem mem_sumSq : s ∈ sumSq T ↔ IsSumSq s := Iff.rfl
+
+end AddSubmonoid
+
+@[deprecated (since := "2024-08-09")] alias SumSqIn := AddSubmonoid.sumSq
+@[deprecated (since := "2025-01-03")] alias sumSqIn := AddSubmonoid.sumSq
+@[deprecated (since := "2025-01-06")] alias sumSq := AddSubmonoid.sumSq
 
 /--
-In an additive monoid with multiplication, every square is a sum of squares. By definition, a square
-in `R` is a term `x : R` such that `x = y * y` for some `y : R` and in Mathlib this is known as
-`IsSquare R` (see Mathlib.Algebra.Group.Even).
+In an additive monoid with multiplication, squares are sums of squares
+(see Mathlib.Algebra.Group.Even).
 -/
-theorem mem_sumSq_of_isSquare [AddMonoid R] {x : R} (px : IsSquare x) : x ∈ sumSq R := by
-  rcases px with ⟨y, py⟩
-  rw [py, ← AddMonoid.add_zero (y * y)]
-  exact IsSumSq.sq_add _ _ IsSumSq.zero
+theorem mem_sumSq_of_isSquare [AddMonoid R] [Mul R] {x : R} (hx : IsSquare x) :
+    x ∈ AddSubmonoid.sumSq R := by
+  rcases hx with ⟨y, hy⟩
+  rw [hy, ← AddMonoid.add_zero (y * y)]
+  exact IsSumSq.sq_add _ IsSumSq.zero
 
 @[deprecated (since := "2024-08-09")] alias SquaresInSumSq := mem_sumSq_of_isSquare
 @[deprecated (since := "2025-01-03")] alias mem_sumSqIn_of_isSquare := mem_sumSq_of_isSquare
 
 /--
 In an additive monoid with multiplication `R`, the submonoid generated by the squares is the set of
-sums of squares.
+sums of squares in `R`.
 -/
-theorem AddSubmonoid.closure_isSquare [AddMonoid R] : closure {x : R | IsSquare x} = sumSq R := by
+theorem AddSubmonoid.closure_isSquare [AddMonoid R] [Mul R] :
+    closure {x : R | IsSquare x} = sumSq R := by
   refine le_antisymm (closure_le.2 (fun x hx ↦ mem_sumSq_of_isSquare hx)) (fun x hx ↦ ?_)
-  induction hx with
-  | zero             => exact zero_mem _
-  | sq_add a S _ ih  => exact AddSubmonoid.add_mem _ (subset_closure ⟨a, rfl⟩) ih
+  induction hx <;> aesop
 
 @[deprecated (since := "2024-08-09")] alias SquaresAddClosure := AddSubmonoid.closure_isSquare
 
 /--
-Let `R` be a linearly ordered semiring in which the property `a ≤ b → ∃ c, a + c = b` holds
-(e.g. `R = ℕ`). If `S : R` is a sum of squares in `R`, then `0 ≤ S`. This is used in
-`Mathlib.Algebra.Ring.Semireal.Defs` to show that linearly ordered fields are semireal.
+In an additive commutative monoid with multiplication,
+`∑ i ∈ I, a i * a i` is a sum of squares.
+-/
+theorem IsSumSq.sum_mul_self [AddCommMonoid R] [Mul R] {ι : Type*} (I : Finset ι) (a : ι → R) :
+    IsSumSq (∑ i ∈ I, a i * a i) := by
+  induction I using Finset.cons_induction with
+  | empty         => simpa using IsSumSq.zero
+  | cons i _ hi h => exact (Finset.sum_cons (β := R) hi) ▸ IsSumSq.sq_add (a i) h
+
+@[deprecated (since := "2024-12-27")] alias isSumSq_sum_mul_self := IsSumSq.sum_mul_self
+
+/--
+In a linearly ordered semiring with the property `a ≤ b → ∃ c, a + c = b` (e.g. `ℕ`),
+sums of squares are non-negative.
 -/
-theorem IsSumSq.nonneg {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R] {S : R}
-    (pS : IsSumSq S) : 0 ≤ S := by
-  induction pS with
-  | zero             => simp only [le_refl]
-  | sq_add x S _ ih  => apply add_nonneg ?_ ih; simp only [← pow_two x, sq_nonneg]
+theorem IsSumSq.nonneg {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R] {s : R}
+    (hs : IsSumSq s) : 0 ≤ s := by
+  induction hs with
+  | zero           => simp only [le_refl]
+  | sq_add x _ ih  => apply add_nonneg ?_ ih; simp only [← pow_two x, sq_nonneg]
 
 @[deprecated (since := "2024-08-09")] alias isSumSq.nonneg := IsSumSq.nonneg