roots_charpoly_eq_eigenvalues — Mathlib

English

The roots of the characteristic polynomial of a Hermitian matrix correspond exactly to its eigenvalues (real).

Русский

Корни характеристического многочлена эрмитовой матрицы точно совпадают с её собственными значениями (реальные).

LaTeX

$$$A.charpoly.roots = \{ h_A.eigenvalues_i : i \in \mathrm{Fin}(\mathrm{card}\ n)\}$$$

Lean4

theorem roots_charpoly_eq_eigenvalues :
    A.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) Finset.univ.val :=
  by
  rw [hA.charpoly_eq, Polynomial.roots_prod]
  · simp
  · simp [Finset.prod_ne_zero_iff, Polynomial.X_sub_C_ne_zero]

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