suggestions

Author: themathqueen

Mathlib/Analysis/Matrix/Order.lean

@@ -44,13 +44,9 @@ attribute [aesop 20% apply (rule_sets := [CStarAlgebra])] PosSemidef.nonneg
 /-- The partial order on matrices given by `A ≤ B := (B - A).PosSemidef`. -/
 abbrev instPartialOrder : PartialOrder (Matrix n n 𝕜) where
   le_antisymm A B h₁ h₂ := by
-    have foo := neg_nonneg.mp <| trace_neg (A - B) ▸ neg_sub A B ▸ h₁.trace_nonneg
-    have : (A - B).trace = 0 := le_antisymm foo h₂.trace_nonneg
-    classical
-    simp_rw [h₂.isHermitian.trace_eq_sum_eigenvalues, ← RCLike.ofReal_sum,
-      RCLike.ofReal_eq_zero, Finset.sum_eq_zero_iff_of_nonneg (s := Finset.univ)
-        (by simpa using h₂.eigenvalues_nonneg), Finset.mem_univ, true_imp_iff] at this
-    exact sub_eq_zero.mp <| funext_iff.eq ▸ h₂.isHermitian.eigenvalues_eq_zero_iff.mp <| this
+    rw [← sub_eq_zero, ← h₂.trace_eq_zero_iff]
+    have := neg_nonneg.mp <| trace_neg (A - B) ▸ neg_sub A B ▸ h₁.trace_nonneg
+    exact le_antisymm this h₂.trace_nonneg
 
 scoped[MatrixOrder] attribute [instance] Matrix.instPartialOrder
 
@@ -110,11 +106,11 @@ lemma sq_sqrt : (CFC.sqrt A) ^ 2 = A := CFC.sq_sqrt A
 @[deprecated CFC.sqrt_mul_sqrt_self (since := "2025-09-22")]
 lemma sqrt_mul_self : CFC.sqrt A * CFC.sqrt A = A := CFC.sqrt_mul_sqrt_self A
 
-lemma eq_of_sq_eq_sq {B : Matrix n n 𝕜} (hB : PosSemidef B) (hAB : A ^ 2 = B ^ 2) : A = B :=
-  CFC.sqrt_sq A ▸ CFC.sqrt_unique (sq B ▸ hAB.symm)
-
+@[deprecated CFC.sq_eq_sq_iff (since := "2025-09-24")]
 lemma sq_eq_sq_iff {B : Matrix n n 𝕜} (hB : PosSemidef B) : A ^ 2 = B ^ 2 ↔ A = B :=
-  ⟨eq_of_sq_eq_sq hA hB, fun h => h ▸ rfl⟩
+  CFC.sq_eq_sq_iff A B
+
+@[deprecated (since := "2025-09-24")] alias ⟨eq_of_sq_eq_sq, _⟩ := CFC.sq_eq_sq_iff
 
 @[deprecated CFC.sqrt_sq (since := "2025-09-22")]
 lemma sqrt_sq : CFC.sqrt (A ^ 2) = A := CFC.sqrt_sq A

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

@@ -277,6 +277,10 @@ lemma sqrt_eq_iff (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc
 lemma sqrt_eq_zero_iff (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt a = 0 ↔ a = 0 := by
   rw [sqrt_eq_iff a _, mul_zero, eq_comm]
 
+lemma mul_self_eq_mul_self_iff (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) :
+    a * a = b * b ↔ a = b :=
+  ⟨fun h => sqrt_mul_self a ▸ sqrt_unique h.symm, fun h => h ▸ rfl⟩
+
 /-- Note that the hypothesis `0 ≤ a` is necessary because the continuous functional calculi over
 `ℝ≥0` (for the left-hand side) and `ℝ` (for the right-hand side) use different predicates (i.e.,
 `(0 ≤ ·)` versus `IsSelfAdjoint`). Consequently, if `a` is selfadjoint but not nonnegative, then
@@ -596,6 +600,10 @@ lemma sqrt_sq (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt (a ^ 2) = a := by
 lemma sq_sqrt (a : A) (ha : 0 ≤ a := by cfc_tac) : (sqrt a) ^ 2 = a := by
   rw [pow_two, sqrt_mul_sqrt_self (A := A) a]
 
+lemma sq_eq_sq_iff (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) :
+    a ^ 2 = b ^ 2 ↔ a = b := by
+  simp_rw [sq, mul_self_eq_mul_self_iff a b]
+
 @[simp]
 lemma sqrt_algebraMap {r : ℝ≥0} : sqrt (algebraMap ℝ≥0 A r) = algebraMap ℝ≥0 A (NNReal.sqrt r) := by
   rw [sqrt_eq_cfc, cfc_algebraMap]

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -239,6 +239,15 @@ lemma IsHermitian.posSemidef_iff_eigenvalues_nonneg [DecidableEq n] {A : Matrix
 @[deprecated (since := "2025-08-17")] alias ⟨_, IsHermitian.posSemidef_of_eigenvalues_nonneg⟩ :=
   IsHermitian.posSemidef_iff_eigenvalues_nonneg
 
+theorem PosSemidef.trace_eq_zero_iff {A : Matrix n n 𝕜} (hA : A.PosSemidef) :
+    A.trace = 0 ↔ A = 0 := by
+  refine ⟨fun h => ?_, fun h => h ▸ trace_zero n 𝕜⟩
+  classical
+  simp_rw [hA.isHermitian.trace_eq_sum_eigenvalues, ← RCLike.ofReal_sum,
+    RCLike.ofReal_eq_zero, Finset.sum_eq_zero_iff_of_nonneg (s := Finset.univ)
+      (by simpa using hA.eigenvalues_nonneg), Finset.mem_univ, true_imp_iff] at h
+  exact funext_iff.eq ▸ hA.isHermitian.eigenvalues_eq_zero_iff.mp <| h
+
 /-!
 ## Positive definite matrices
 -/