mem_spectrum_iff_isRoot_charpoly — Mathlib

English

μ ∈ spectrum(K,f) if and only if μ is a root of the charpoly of f.

Русский

μ принадлежит спектруму f тогда и только тогда, когда μ является корнем характеристического многочлена f.

LaTeX

$$$μ \\in \\mathrm{spectrum}(K,f) \\iff (\\mathrm{charpoly}(f)).IsRoot(μ)$$$

Lean4

theorem mem_spectrum_iff_isRoot_charpoly (f : End K V) (μ : K) : μ ∈ spectrum K f ↔ f.charpoly.IsRoot μ := by
  rw [← hasEigenvalue_iff_mem_spectrum, hasEigenvalue_iff_isRoot_charpoly]

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