splits_charpoly — Mathlib

English

The characteristic polynomial of a Hermitian matrix splits over the base field; it factors completely into linear terms.

Русский

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

LaTeX

$$A.charpoly.Splits(id 𝕜)$$

Lean4

theorem splits_charpoly (hA : A.IsHermitian) : A.charpoly.Splits (RingHom.id 𝕜) :=
  Polynomial.splits_iff_card_roots.mpr (by simp [hA.roots_charpoly_eq_eigenvalues])

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