feat: eigenvalues of AᴴA and AAᴴ are non-negative (#7312)

The PR provides two  lemmas showing that the eigenvalues of $A\^HA$ and $AA^H$ are non-negative:

- `eigenvalues_conjTranspose_mul_self_nonneg`:
$$\text{eig}(A\^H A) \geq 0 $$
- `eigenvalues_self_mul_conjTranspose_nonneg`:
$$\text{eig}(A A\^H) \geq 0 $$

This was suggested by @Vierkantor in PR #6042

Author: MohanadAhmed

Mathlib/LinearAlgebra/Matrix/PosDef.lean

@@ -130,6 +130,14 @@ lemma PosSemidef.eigenvalues_nonneg [DecidableEq n] {A : Matrix n n 𝕜}
     (hA : Matrix.PosSemidef A) (i : n) : 0 ≤ hA.1.eigenvalues i :=
   (hA.re_dotProduct_nonneg _).trans_eq (hA.1.eigenvalues_eq _).symm
 
+lemma eigenvalues_conjTranspose_mul_self_nonneg (A : Matrix m n 𝕜) [DecidableEq n] (i : n) :
+    0 ≤ (isHermitian_transpose_mul_self A).eigenvalues i :=
+  (Matrix.posSemidef_conjTranspose_mul_self _).eigenvalues_nonneg _
+
+lemma eigenvalues_self_mul_conjTranspose_nonneg (A : Matrix m n 𝕜) [DecidableEq m] (i : m) :
+    0 ≤ (isHermitian_mul_conjTranspose_self A).eigenvalues i :=
+  (Matrix.posSemidef_self_mul_conjTranspose _).eigenvalues_nonneg _
+
 namespace PosDef
 
 variable {M : Matrix n n ℝ} (hM : M.PosDef)