feat: make StarOrderedRing a mixin (#11872)

This makes `StarOrderedRing` take `StarRing` as a parameter instead of extending it, and as a result moves the typeclass to `Prop`. It was already a mixin with respect to the order and algebraic structure. There are two primary motivations:

1. This makes it possible to directly assume that `C(α, R)` is a `StarOrderedRing` with `[StarOrderedRing C(α, R)]`, as currently there is no typeclass on `R` which would naturally guarantee this property. This is relevant as we want this type class on continuous functions for the continuous functional calculus.
2. We will eventually want a `StarOrderedRing` instance on `C(α, A)` where `A` is a complex (or even real) C⋆-algebra, and making this a mixin avoids loops with `StarRing`.

Mathlib/Algebra/Order/Ring/Star.lean

@@ -25,15 +25,15 @@ namespace StarOrderedRing
 must commute. We provide this only as an example as opposed to a lemma because we never expect the
 type class assumptions to be satisfied without a `CommSemiring` intance already in scope; not that
 it is impossible, only that it shouldn't occur in practice. -/
-example {R : Type*} [OrderedSemiring R] [StarOrderedRing R] {x y : R} (hx : 0 ≤ x) (hy : 0 ≤ y) :
-    x * y = y * x := by
+example {R : Type*} [OrderedSemiring R] [StarRing R] [StarOrderedRing R] {x y : R} (hx : 0 ≤ x)
+    (hy : 0 ≤ y) : x * y = y * x := by
   rw [← IsSelfAdjoint.of_nonneg (mul_nonneg hy hx), star_mul, IsSelfAdjoint.of_nonneg hx,
     IsSelfAdjoint.of_nonneg hy]
 
 /- This will be implied by the instance below, we only prove it to avoid duplicating the
 argument in the instance below for `mul_le_mul_of_nonneg_right`. -/
 private lemma mul_le_mul_of_nonneg_left {R : Type*} [CommSemiring R] [PartialOrder R]
-    [StarOrderedRing R] {a b c : R} (hab : a ≤ b) (hc : 0 ≤ c) : c * a ≤ c * b := by
+    [StarRing R] [StarOrderedRing R] {a b c : R} (hab : a ≤ b) (hc : 0 ≤ c) : c * a ≤ c * b := by
   rw [StarOrderedRing.nonneg_iff] at hc
   induction hc using AddSubmonoid.closure_induction' with
   | mem _ h =>
@@ -53,7 +53,7 @@ and `OrderedCommSemiring`, and it seem loops still cause issues sometimes.
 See note [reducible non-instances]. -/
 @[reducible]
 def toOrderedCommSemiring (R : Type*) [CommSemiring R] [PartialOrder R]
-    [StarOrderedRing R] : OrderedCommSemiring R where
+    [StarRing R] [StarOrderedRing R] : OrderedCommSemiring R where
   add_le_add_left _ _ := add_le_add_left
   zero_le_one := by simpa using star_mul_self_nonneg (1 : R)
   mul_comm := mul_comm
@@ -68,7 +68,7 @@ and `OrderedCommSemiring`, and it seem loops still cause issues sometimes.
 See note [reducible non-instances]. -/
 @[reducible]
 def toOrderedCommRing (R : Type*) [CommRing R] [PartialOrder R]
-    [StarOrderedRing R] : OrderedCommRing R where
+    [StarRing R] [StarOrderedRing R] : OrderedCommRing R where
   add_le_add_left _ _ := add_le_add_left
   zero_le_one := by simpa using star_mul_self_nonneg (1 : R)
   mul_comm := mul_comm

Mathlib/Algebra/Star/CHSH.lean

@@ -118,7 +118,7 @@ set_option linter.uppercaseLean3 false in
 
 (We could work over ℤ[⅟2] if we wanted to!)
 -/
-theorem CHSH_inequality_of_comm [OrderedCommRing R] [StarOrderedRing R] [Algebra ℝ R]
+theorem CHSH_inequality_of_comm [OrderedCommRing R] [StarRing R] [StarOrderedRing R] [Algebra ℝ R]
     [OrderedSMul ℝ R] (A₀ A₁ B₀ B₁ : R) (T : IsCHSHTuple A₀ A₁ B₀ B₁) :
     A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2 := by
   let P := 2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁
@@ -183,8 +183,8 @@ of the difference.
 
 (We could work over `ℤ[2^(1/2), 2^(-1/2)]` if we really wanted to!)
 -/
-theorem tsirelson_inequality [OrderedRing R] [StarOrderedRing R] [Algebra ℝ R] [OrderedSMul ℝ R]
-    [StarModule ℝ R] (A₀ A₁ B₀ B₁ : R) (T : IsCHSHTuple A₀ A₁ B₀ B₁) :
+theorem tsirelson_inequality [OrderedRing R] [StarRing R] [StarOrderedRing R] [Algebra ℝ R]
+    [OrderedSMul ℝ R] [StarModule ℝ R] (A₀ A₁ B₀ B₁ : R) (T : IsCHSHTuple A₀ A₁ B₀ B₁) :
     A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • (1 : R) := by
   -- abel will create `ℤ` multiplication. We will `simp` them away to `ℝ` multiplication.
   have M : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = ((m : ℝ) * a) • x := fun m a x => by

Mathlib/Algebra/Star/Order.lean

@@ -49,7 +49,7 @@ convenient to declare instances using `StarOrderedRing.ofNonnegIff'`.
 
 Porting note: dropped an unneeded assumption
 `add_le_add_left : ∀ {x y}, x ≤ y → ∀ z, z + x ≤ z + y` -/
-class StarOrderedRing (R : Type u) [NonUnitalSemiring R] [PartialOrder R] extends StarRing R where
+class StarOrderedRing (R : Type u) [NonUnitalSemiring R] [PartialOrder R] [StarRing R] : Prop where
   /-- characterization of the order in terms of the `StarRing` structure. -/
   le_iff :
     ∀ x y : R, x ≤ y ↔ ∃ p, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p
@@ -59,7 +59,7 @@ namespace StarOrderedRing
 
 -- see note [lower instance priority]
 instance (priority := 100) toOrderedAddCommMonoid [NonUnitalSemiring R] [PartialOrder R]
-    [StarOrderedRing R] : OrderedAddCommMonoid R where
+    [StarRing R] [StarOrderedRing R] : OrderedAddCommMonoid R where
   add_le_add_left := fun x y hle z ↦ by
     rw [StarOrderedRing.le_iff] at hle ⊢
     refine hle.imp fun s hs ↦ ?_
@@ -69,20 +69,19 @@ instance (priority := 100) toOrderedAddCommMonoid [NonUnitalSemiring R] [Partial
 
 -- see note [lower instance priority]
 instance (priority := 100) toExistsAddOfLE [NonUnitalSemiring R] [PartialOrder R]
-    [StarOrderedRing R] : ExistsAddOfLE R where
+    [StarRing R] [StarOrderedRing R] : ExistsAddOfLE R where
   exists_add_of_le h :=
     match (le_iff _ _).mp h with
     | ⟨p, _, hp⟩ => ⟨p, hp⟩
 #align star_ordered_ring.to_has_exists_add_of_le StarOrderedRing.toExistsAddOfLE
 
 -- see note [lower instance priority]
 instance (priority := 100) toOrderedAddCommGroup [NonUnitalRing R] [PartialOrder R]
-    [StarOrderedRing R] : OrderedAddCommGroup R where
+    [StarRing R] [StarOrderedRing R] : OrderedAddCommGroup R where
   add_le_add_left := @add_le_add_left _ _ _ _
 
 #align star_ordered_ring.to_ordered_add_comm_group StarOrderedRing.toOrderedAddCommGroup
 
--- set note [reducible non-instances]
 /-- To construct a `StarOrderedRing` instance it suffices to show that `x ≤ y` if and only if
 `y = x + star s * s` for some `s : R`.
 
@@ -92,8 +91,7 @@ and obviates the hassle of `AddSubmonoid.closure_induction` when creating those
 If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, see
 `StarOrderedRing.ofNonnegIff` for a more convenient version.
  -/
-@[reducible]
-def ofLEIff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
+lemma ofLEIff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
     (h_le_iff : ∀ x y : R, x ≤ y ↔ ∃ s, y = x + star s * s) : StarOrderedRing R where
   le_iff x y := by
     refine' ⟨fun h => _, _⟩
@@ -109,12 +107,10 @@ def ofLEIff [NonUnitalSemiring R] [PartialOrder R] [StarRing R]
         exact (ha _ _ rfl).trans (hb _ _ rfl)
 #align star_ordered_ring.of_le_iff StarOrderedRing.ofLEIffₓ
 
--- set note [reducible non-instances]
 /-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
 show that the nonnegative elements are precisely those elements in the `AddSubmonoid` generated
 by `star s * s` for `s : R`. -/
-@[reducible]
-def ofNonnegIff [NonUnitalRing R] [PartialOrder R] [StarRing R]
+lemma ofNonnegIff [NonUnitalRing R] [PartialOrder R] [StarRing R]
     (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
     (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s)) :
     StarOrderedRing R where
@@ -123,24 +119,22 @@ def ofNonnegIff [NonUnitalRing R] [PartialOrder R] [StarRing R]
     simpa only [← sub_eq_iff_eq_add', sub_nonneg, exists_eq_right'] using h_nonneg_iff (y - x)
 #align star_ordered_ring.of_nonneg_iff StarOrderedRing.ofNonnegIff
 
--- set note [reducible non-instances]
 /-- When `R` is a non-unital ring, to construct a `StarOrderedRing` instance it suffices to
 show that the nonnegative elements are precisely those elements of the form `star s * s`
 for `s : R`.
 
 This is provided for convenience because it holds in many common scenarios (e.g.,`ℝ`, `ℂ`, or
 any C⋆-algebra), and obviates the hassle of `AddSubmonoid.closure_induction` when creating those
 instances. -/
-@[reducible]
-def ofNonnegIff' [NonUnitalRing R] [PartialOrder R] [StarRing R]
+lemma ofNonnegIff' [NonUnitalRing R] [PartialOrder R] [StarRing R]
     (h_add : ∀ {x y : R}, x ≤ y → ∀ z, z + x ≤ z + y)
     (h_nonneg_iff : ∀ x : R, 0 ≤ x ↔ ∃ s, x = star s * s) : StarOrderedRing R :=
   ofLEIff <| by
     haveI : CovariantClass R R (· + ·) (· ≤ ·) := ⟨fun _ _ _ h => h_add h _⟩
     simpa [sub_eq_iff_eq_add', sub_nonneg] using fun x y => h_nonneg_iff (y - x)
 #align star_ordered_ring.of_nonneg_iff' StarOrderedRing.ofNonnegIff'
 
-theorem nonneg_iff [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R] {x : R} :
+theorem nonneg_iff [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R] {x : R} :
     0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s) := by
   simp only [le_iff, zero_add, exists_eq_right']
 #align star_ordered_ring.nonneg_iff StarOrderedRing.nonneg_iff
@@ -149,7 +143,7 @@ end StarOrderedRing
 
 section NonUnitalSemiring
 
-variable [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R]
+variable [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
 
 theorem star_mul_self_nonneg (r : R) : 0 ≤ star r * r :=
   StarOrderedRing.nonneg_iff.mpr <| AddSubmonoid.subset_closure ⟨r, rfl⟩
@@ -241,7 +235,7 @@ lemma IsSelfAdjoint.of_nonneg {x : R} (hx : 0 ≤ x) : IsSelfAdjoint x :=
 end NonUnitalSemiring
 
 section Semiring
-variable [Semiring R] [PartialOrder R] [StarOrderedRing R]
+variable [Semiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
 
 @[simp]
 lemma one_le_star_iff {x : R} : 1 ≤ star x ↔ 1 ≤ x := by
@@ -263,8 +257,8 @@ end Semiring
 
 section OrderClass
 
-variable {F R S : Type*} [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R]
-variable [NonUnitalSemiring S] [PartialOrder S] [StarOrderedRing S]
+variable {F R S : Type*} [NonUnitalSemiring R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
+variable [NonUnitalSemiring S] [PartialOrder S] [StarRing S] [StarOrderedRing S]
 
 -- we prove this auxiliary lemma in order to avoid duplicating the proof twice below.
 lemma NonUnitalRingHom.map_le_map_of_map_star (f : R →ₙ+* S) (hf : ∀ r, f (star r) = star (f r))

Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus/Instances.lean

@@ -248,7 +248,7 @@ end SpectrumRestricts
 section Nonneg
 
 variable {A : Type*} [NormedRing A] [CompleteSpace A]
-variable [PartialOrder A] [StarOrderedRing A] [CstarRing A]
+variable [PartialOrder A] [StarRing A] [StarOrderedRing A] [CstarRing A]
 variable [NormedAlgebra ℂ A] [StarModule ℂ A]
 
 lemma nonneg_iff_isSelfAdjoint_and_spectrumRestricts {a : A} :

Mathlib/Analysis/RCLike/Basic.lean

@@ -883,7 +883,7 @@ lemma neg_iff_exists_ofReal : z < 0 ↔ ∃ x < (0 : ℝ), x = z := by
 (That is, a star ring in which the nonnegative elements are those of the form `star z * z`.)
 
 Note this is only an instance with `open scoped ComplexOrder`. -/
-def toStarOrderedRing : StarOrderedRing K :=
+lemma toStarOrderedRing : StarOrderedRing K :=
   StarOrderedRing.ofNonnegIff'
     (h_add := fun {x y} hxy z => by
       rw [RCLike.le_iff_re_im] at *

Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

@@ -87,8 +87,8 @@ theorem lapMatrix_toLinearMap₂' [Field α] [CharZero α] (x : V → α) :
   ring_nf
 
 /-- The Laplacian matrix is positive semidefinite -/
-theorem posSemidef_lapMatrix [LinearOrderedField α] [StarOrderedRing α] [TrivialStar α] :
-    PosSemidef (G.lapMatrix α) := by
+theorem posSemidef_lapMatrix [LinearOrderedField α] [StarRing α] [StarOrderedRing α]
+    [TrivialStar α] : PosSemidef (G.lapMatrix α) := by
   constructor
   · rw [IsHermitian, conjTranspose_eq_transpose_of_trivial, isSymm_lapMatrix]
   · intro x

Mathlib/Data/Matrix/Rank.lean

@@ -209,7 +209,7 @@ be replaced with a proof that uses Gaussian reduction or argues via linear combi
 
 section StarOrderedField
 
-variable [Fintype m] [Field R] [PartialOrder R] [StarOrderedRing R]
+variable [Fintype m] [Field R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
 
 theorem ker_mulVecLin_conjTranspose_mul_self (A : Matrix m n R) :
     LinearMap.ker (Aᴴ * A).mulVecLin = LinearMap.ker (mulVecLin A) := by

Mathlib/LinearAlgebra/Matrix/DotProduct.lean

@@ -99,19 +99,19 @@ theorem dotProduct_self_eq_zero [LinearOrderedRing R] {v : n → R} : dotProduct
 
 section StarOrderedRing
 
-variable [PartialOrder R] [NonUnitalRing R] [StarOrderedRing R] [NoZeroDivisors R]
+variable [PartialOrder R] [NonUnitalRing R] [StarRing R] [StarOrderedRing R] [NoZeroDivisors R]
 
 /-- Note that this applies to `ℂ` via `Complex.strictOrderedCommRing`. -/
 @[simp]
 theorem dotProduct_star_self_eq_zero {v : n → R} : dotProduct (star v) v = 0 ↔ v = 0 :=
-  (Finset.sum_eq_zero_iff_of_nonneg fun i _ => (@star_mul_self_nonneg _ _ _ _ (v i) : _)).trans <|
+  (Finset.sum_eq_zero_iff_of_nonneg fun i _ => (star_mul_self_nonneg (r := v i) : _)).trans <|
     by simp [Function.funext_iff, mul_eq_zero]
 #align matrix.dot_product_star_self_eq_zero Matrix.dotProduct_star_self_eq_zero
 
 /-- Note that this applies to `ℂ` via `Complex.strictOrderedCommRing`. -/
 @[simp]
 theorem dotProduct_self_star_eq_zero {v : n → R} : dotProduct v (star v) = 0 ↔ v = 0 :=
-  (Finset.sum_eq_zero_iff_of_nonneg fun i _ => (@mul_star_self_nonneg _ _ _ _ (v i) : _)).trans <|
+  (Finset.sum_eq_zero_iff_of_nonneg fun i _ => (mul_star_self_nonneg (r := v i) : _)).trans <|
     by simp [Function.funext_iff, mul_eq_zero]
 #align matrix.dot_product_self_star_eq_zero Matrix.dotProduct_self_star_eq_zero
 

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -34,7 +34,7 @@ namespace Matrix
 
 variable {m n R 𝕜 : Type*}
 variable [Fintype m] [Fintype n]
-variable [CommRing R] [PartialOrder R] [StarOrderedRing R]
+variable [CommRing R] [PartialOrder R] [StarRing R] [StarOrderedRing R]
 variable [RCLike 𝕜]
 open scoped Matrix
 

Mathlib/LinearAlgebra/Matrix/SchurComplement.lean

@@ -477,7 +477,7 @@ end CommRing
 
 section StarOrderedRing
 
-variable {𝕜 : Type*} [CommRing 𝕜] [PartialOrder 𝕜] [StarOrderedRing 𝕜]
+variable {𝕜 : Type*} [CommRing 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜]
 
 scoped infixl:65 " ⊕ᵥ " => Sum.elim