chore: rename star_mul_self_nonneg' (#8305)

j-loreaux · j-loreaux · commit 7a1bf932d49a · 2023-11-10T10:42:45.000Z
diff --git a/Mathlib/Algebra/Star/Order.lean b/Mathlib/Algebra/Star/Order.lean
@@ -152,9 +152,9 @@ theorem star_mul_self_nonneg (r : R) : 0 ≤ star r * r :=
   StarOrderedRing.nonneg_iff.mpr <| AddSubmonoid.subset_closure ⟨r, rfl⟩
 #align star_mul_self_nonneg star_mul_self_nonneg
 
-theorem star_mul_self_nonneg' (r : R) : 0 ≤ r * star r := by
+theorem mul_star_self_nonneg (r : R) : 0 ≤ r * star r := by
   simpa only [star_star] using star_mul_self_nonneg (star r)
-#align star_mul_self_nonneg' star_mul_self_nonneg'
+#align star_mul_self_nonneg' mul_star_self_nonneg
 
 theorem conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c := by
   rw [StarOrderedRing.nonneg_iff] at ha
diff --git a/Mathlib/LinearAlgebra/Matrix/DotProduct.lean b/Mathlib/LinearAlgebra/Matrix/DotProduct.lean
@@ -94,7 +94,7 @@ theorem dotProduct_star_self_eq_zero {v : n → R} : dotProduct (star v) v = 0 
 /-- 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 _ => (@star_mul_self_nonneg' _ _ _ _ (v i) : _)).trans <|
+  (Finset.sum_eq_zero_iff_of_nonneg fun i _ => (@mul_star_self_nonneg _ _ _ _ (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
 
