chore(LinearAlgebra/Matrix/Hermitian): fix lemma name (#31484)

`Matrix.isHermitian_transpose_mul_self` should be `Matrix.isHermitian_conjTranspose_mul_self`.

Author: themathqueen

Mathlib/LinearAlgebra/Matrix/Hermitian.lean

@@ -184,9 +184,13 @@ theorem isHermitian_mul_conjTranspose_self [Fintype n] (A : Matrix m n α) :
     (A * Aᴴ).IsHermitian := by rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
 
 /-- Note this is more general than `IsSelfAdjoint.star_mul_self` as `B` can be rectangular. -/
-theorem isHermitian_transpose_mul_self [Fintype m] (A : Matrix m n α) : (Aᴴ * A).IsHermitian := by
+theorem isHermitian_conjTranspose_mul_self [Fintype m] (A : Matrix m n α) :
+    (Aᴴ * A).IsHermitian := by
   rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]
 
+@[deprecated (since := "2025-11-10")] alias isHermitian_transpose_mul_self :=
+  isHermitian_conjTranspose_mul_self
+
 /-- Note this is more general than `IsSelfAdjoint.conjugate'` as `B` can be rectangular. -/
 theorem isHermitian_conjTranspose_mul_mul [Fintype m] {A : Matrix m m α} (B : Matrix m n α)
     (hA : A.IsHermitian) : (Bᴴ * A * B).IsHermitian := by

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -203,7 +203,7 @@ theorem posSemidef_submatrix_equiv {M : Matrix n n R} (e : m ≃ n) :
 /-- The conjugate transpose of a matrix multiplied by the matrix is positive semidefinite -/
 theorem posSemidef_conjTranspose_mul_self [StarOrderedRing R] (A : Matrix m n R) :
     PosSemidef (Aᴴ * A) := by
-  refine ⟨isHermitian_transpose_mul_self _, fun x => ?_⟩
+  refine ⟨isHermitian_conjTranspose_mul_self _, fun x => ?_⟩
   rw [← mulVec_mulVec, dotProduct_mulVec, vecMul_conjTranspose, star_star]
   exact Finset.sum_nonneg fun i _ => star_mul_self_nonneg _
 
@@ -235,7 +235,7 @@ theorem trace_mul_conjTranspose_self_eq_zero_iff {A : Matrix m n R} :
 end trace
 
 lemma eigenvalues_conjTranspose_mul_self_nonneg (A : Matrix m n 𝕜) [DecidableEq n] (i : n) :
-    0 ≤ (isHermitian_transpose_mul_self A).eigenvalues i :=
+    0 ≤ (isHermitian_conjTranspose_mul_self A).eigenvalues i :=
   (posSemidef_conjTranspose_mul_self _).eigenvalues_nonneg _
 
 lemma eigenvalues_self_mul_conjTranspose_nonneg (A : Matrix m n 𝕜) [DecidableEq m] (i : m) :