feat(algebra/star/basic): basic lemmas for star_ordered_ring (#17218)

src/algebra/star/basic.lean

@@ -353,24 +353,51 @@ class star_ordered_ring (R : Type u) [non_unital_semiring R] [partial_order R]
 
 namespace star_ordered_ring
 
-variables [ring R] [partial_order R] [star_ordered_ring R]
-
 @[priority 100] -- see note [lower instance priority]
-instance : ordered_add_comm_group R :=
-{ ..show ring R, by apply_instance,
+instance [non_unital_ring R] [partial_order R] [star_ordered_ring R] : ordered_add_comm_group R :=
+{ ..show non_unital_ring R, by apply_instance,
   ..show partial_order R, by apply_instance,
   ..show star_ordered_ring R, by apply_instance }
 
 end star_ordered_ring
 
-lemma star_mul_self_nonneg
-  [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {r : R} : 0 ≤ star r * r :=
+section non_unital_semiring
+
+variables [non_unital_semiring R] [partial_order R] [star_ordered_ring R]
+
+lemma star_mul_self_nonneg {r : R} : 0 ≤ star r * r :=
 (star_ordered_ring.nonneg_iff _).mpr ⟨r, rfl⟩
 
-lemma star_mul_self_nonneg'
-  [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {r : R} : 0 ≤ r * star r :=
+lemma star_mul_self_nonneg' {r : R} : 0 ≤ r * star r :=
 by { nth_rewrite_rhs 0 [←star_star r], exact star_mul_self_nonneg }
 
+lemma conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c :=
+begin
+  obtain ⟨x, rfl⟩ := (star_ordered_ring.nonneg_iff _).1 ha,
+  exact (star_ordered_ring.nonneg_iff _).2 ⟨x * c, by rw [star_mul, ←mul_assoc, mul_assoc _ _ c]⟩,
+end
+
+lemma conjugate_nonneg' {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c :=
+by simpa only [star_star] using conjugate_nonneg ha (star c)
+
+end non_unital_semiring
+
+section non_unital_ring
+
+variables [non_unital_ring R] [partial_order R] [star_ordered_ring R]
+
+lemma conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) : star c * a * c ≤ star c * b * c :=
+begin
+  rw ←sub_nonneg at hab ⊢,
+  convert conjugate_nonneg hab c,
+  simp only [mul_sub, sub_mul],
+end
+
+lemma conjugate_le_conjugate' {a b : R} (hab : a ≤ b) (c : R) : c * a * star c ≤ c * b * star c :=
+by simpa only [star_star] using conjugate_le_conjugate hab (star c)
+
+end non_unital_ring
+
 /--
 A star module `A` over a star ring `R` is a module which is a star add monoid,
 and the two star structures are compatible in the sense