eigenvalues_pos — Mathlib

English

For every i, the i-th eigenvalue of a positive definite matrix is positive.

Русский

Для каждого индекса i положительно определенной матрицы i-й собственный значения положителен.

LaTeX

$$$$ 0 < h_A.1.eigenvalues(i). $$$$

Lean4

/-- The eigenvalues of a positive definite matrix are positive -/
theorem eigenvalues_pos [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.PosDef A) (i : n) : 0 < hA.1.eigenvalues i :=
  by
  simp only [hA.1.eigenvalues_eq]
  exact hA.re_dotProduct_pos <| hA.1.eigenvectorBasis.orthonormal.ne_zero i

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