mem_spectrum_iff_isRoot_charpoly — Mathlib

English

Over a field K, an element r belongs to the spectrum of A if and only if it is a root of the characteristic polynomial: r ∈ spectrum(K,A) ⇔ A.charpoly.IsRoot(r).

Русский

Над полем K элемент r принадлежит спектру матрицы A тогда и только тогда, когда он является корнем характеристического полинома: r ∈ spectrum(K,A) ⇔ A.charpoly.IsRoot(r).

LaTeX

$$r ∈ \\mathrm{spectrum}(K,A) \\iff A.charpoly.IsRoot(r)$$

Lean4

/-- In fields, the roots of the characteristic polynomial are exactly the spectrum of the matrix.
The weaker direction is true in nontrivial rings (see `Matrix.mem_spectrum_of_isRoot_charpoly`).
-/
theorem mem_spectrum_iff_isRoot_charpoly {r : K} : r ∈ spectrum K A ↔ IsRoot A.charpoly r := by
  simp [eval_charpoly, spectrum.mem_iff, isUnit_iff_isUnit_det, algebraMap_eq_diagonal, Pi.algebraMap_def]

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