rank_eq_rank_diagonal — Mathlib

English

Let A be Hermitian. Then rank(A) equals the rank of the diagonal matrix whose diagonal entries are its eigenvalues.

Русский

Пусть A эрмитов. Тогда ранг(A) равен рангу диагональной матрицы, диагональ которой состоит из его собственных значений.

LaTeX

$$$\\\\operatorname{rank}(A) = \\\\operatorname{rank}(\\\\operatorname{diag}(\\\\lambda_1, \\\\lambda_2, \\\\dots, \\\\lambda_n))$$$

Lean4

/-- rank of a Hermitian matrix is the rank of after diagonalization by the eigenvector unitary -/
theorem rank_eq_rank_diagonal : A.rank = (Matrix.diagonal hA.eigenvalues).rank :=
  by
  conv_lhs => rw [hA.spectral_theorem, ← unitary.coe_star]
  simp [-isUnit_iff_ne_zero, -unitary.coe_star, rank_diagonal]

Похожие утверждения