roots_charpoly_eq_eigenvalues₀ — Mathlib

English

The roots of the characteristic polynomial correspond, via real embedding, to the eigenvalues enumerated by eigenvalues₀.

Русский

Корни характеристического многочлена соответствуют собственным значениям, перечисленным через eigenvalues₀.

LaTeX

$$$A.charpoly.roots = \operatorname{Multiset.map}(\operatorname{RCLike.ofReal} \circ h_A.eigenvalues_0)\; Finset.univ.\val$$$

Lean4

theorem roots_charpoly_eq_eigenvalues₀ :
    A.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues₀) Finset.univ.val :=
  by
  rw [hA.roots_charpoly_eq_eigenvalues]
  simp only [← Multiset.map_map, eigenvalues, ← Function.comp_apply (f := hA.eigenvalues₀)]
  simp

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