rank_eq_card_non_zero_eigs — Mathlib

English

For a Hermitian A, the rank equals the number of nonzero eigenvalues of A.

Русский

Для эрмитова A ранг равен числу ненулевых собственных значений A.

LaTeX

$$$\\\\operatorname{rank}(A) = \\\\#\\\\{ i \\\\mid \\\\lambda_i \\\\neq 0 \\\\}$$$

Lean4

/-- rank of a Hermitian matrix is the number of nonzero eigenvalues of the Hermitian matrix -/
theorem rank_eq_card_non_zero_eigs : A.rank = Fintype.card { i // hA.eigenvalues i ≠ 0 } := by
  rw [rank_eq_rank_diagonal hA, Matrix.rank_diagonal]

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