chore(Algebra/Ring/SumsOfSquares, Algebra/Ring/Semireal): name convension (#15621)

Author: astrainfinita

Mathlib/Algebra/Ring/Semireal/Defs.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Florent Schaffhauser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Florent Schaffhauser
 -/
-
 import Mathlib.Algebra.Ring.SumsOfSquares
 import Mathlib.Algebra.Order.Field.Defs
 
@@ -19,7 +18,7 @@ semireal.
 
 ## Main declaration
 
-- `isSemireal`: the predicate asserting that a commutative ring `R` is semireal.
+- `IsSemireal`: the predicate asserting that a commutative ring `R` is semireal.
 
 ## References
 
@@ -31,14 +30,18 @@ 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`
+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.
 -/
 @[mk_iff]
-class isSemireal [AddMonoid R] [Mul R] [One R] [Neg R] : Prop where
-  non_trivial        : (0 : R) ≠ 1
-  neg_one_not_SumSq  : ¬isSumSq (-1 : R)
+class IsSemireal [AddMonoid R] [Mul R] [One R] [Neg R] : Prop where
+  non_trivial         : (0 : R) ≠ 1
+  not_isSumSq_neg_one : ¬IsSumSq (-1 : R)
+
+@[deprecated (since := "2024-08-09")] alias isSemireal := IsSemireal
+@[deprecated (since := "2024-08-09")] alias isSemireal.neg_one_not_SumSq :=
+  IsSemireal.not_isSumSq_neg_one
 
-instance [LinearOrderedField R] : isSemireal R where
+instance [LinearOrderedField R] : IsSemireal R where
   non_trivial := zero_ne_one
-  neg_one_not_SumSq := fun h ↦ (not_le (α := R)).2 neg_one_lt_zero h.nonneg
+  not_isSumSq_neg_one := fun h ↦ (not_le (α := R)).2 neg_one_lt_zero h.nonneg

Mathlib/Algebra/Ring/SumsOfSquares.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Florent Schaffhauser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Florent Schaffhauser
 -/
-
 import Mathlib.Algebra.Ring.Defs
 import Mathlib.Algebra.Group.Submonoid.Basic
 import Mathlib.Algebra.Group.Even
@@ -13,27 +12,27 @@ 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`:
+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`.
 
 ## Main declaration
 
-- The predicate `isSumSq : R → Prop`, defining the property of being a sum of squares in `R`.
+- The predicate `IsSumSq : R → Prop`, defining the property of being a sum of squares in `R`.
 
 ## Auxiliary declarations
 
-- The type `SumSqIn R` : in an additive monoid with multiplication `R`, we introduce the type
-`SumSqIn R` as the submonoid of `R` whose carrier is the subset `{S : R | isSumSq S}`.
+- The type `sumSqIn R` : in an additive monoid with multiplication `R`, we introduce the type
+`sumSqIn 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`.
-- `SumSq.nonneg`: in a linearly ordered semiring `R` with an `[ExistsAddOfLE R]` instance, sums of
+- `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.
-- `SquaresInSumSq`: a square is a sum of squares.
-- `SquaresAddClosure`: the submonoid of `R` generated by the squares in `R` is the set of sums of
-squares in `R`.
+- `mem_sumSqIn_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`.
 
 -/
 
@@ -45,57 +44,68 @@ squares is defined by an inductive predicate: `0 : R` is a sum of squares and if
 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 [Add R] [Zero R] : R → Prop
+  | zero                              : IsSumSq 0
+  | sq_add (a S : R) (pS : 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`.
 -/
-theorem isSumSq.add [AddMonoid R] {S1 S2 : R} (p1 : isSumSq S1)
-    (p2 : isSumSq S2) : isSumSq (S1 + S2) := by
+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
+  | sq_add a S pS ih => rw [add_assoc]; exact IsSumSq.sq_add a (S + S2) ih
+
+@[deprecated (since := "2024-08-09")] alias isSumSq.add := IsSumSq.add
 
 variable (R) in
 /--
-In an additive monoid with multiplication `R`, the type `SumSqIn R` is the submonoid of sums of
+In an additive monoid with multiplication `R`, the type `sumSqIn R` is the submonoid of sums of
 squares in `R`.
 -/
-def SumSqIn [AddMonoid R] : AddSubmonoid R where
-  carrier   := {S : R | isSumSq S}
-  zero_mem' := isSumSq.zero
-  add_mem'  := isSumSq.add
+def sumSqIn [AddMonoid R] : AddSubmonoid R where
+  carrier   := {S : R | IsSumSq S}
+  zero_mem' := IsSumSq.zero
+  add_mem'  := IsSumSq.add
+
+@[deprecated (since := "2024-08-09")] alias SumSqIn := sumSqIn
 
 /--
 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).
 -/
-theorem SquaresInSumSq [AddMonoid R] {x : R} (px : IsSquare x) : x ∈ SumSqIn R := by
+theorem mem_sumSqIn_of_isSquare [AddMonoid R] {x : R} (px : IsSquare x) : x ∈ sumSqIn R := by
   rcases px with ⟨y, py⟩
   rw [py, ← AddMonoid.add_zero (y * y)]
-  exact isSumSq.sq_add _ _ isSumSq.zero
+  exact IsSumSq.sq_add _ _ IsSumSq.zero
+
+@[deprecated (since := "2024-08-09")] alias SquaresInSumSq := mem_sumSqIn_of_isSquare
 
-open AddSubmonoid in
 /--
 In an additive monoid with multiplication `R`, the submonoid generated by the squares is the set of
 sums of squares.
 -/
-theorem SquaresAddClosure [AddMonoid R] : closure IsSquare = SumSqIn R := by
-  refine le_antisymm (closure_le.2 (fun x hx ↦ SquaresInSumSq hx)) (fun x hx ↦ ?_)
+theorem AddSubmonoid.closure_isSquare [AddMonoid R] : closure {x : R | IsSquare x} = sumSqIn R := by
+  refine le_antisymm (closure_le.2 (fun x hx ↦ mem_sumSqIn_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
 
+@[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.
 -/
-theorem isSumSq.nonneg {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R] {S : R}
-    (pS : isSumSq S) : 0 ≤ S := by
+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]
+
+@[deprecated (since := "2024-08-09")] alias isSumSq.nonneg := IsSumSq.nonneg