mem_spectrum_of_isRoot_charpoly — Mathlib

English

The roots of the characteristic polynomial belong to the spectrum of the matrix.

Русский

Корни характеристического полинома принадлежат спектру матрицы.

LaTeX

$$If $hr$ is a root of $B.charpoly$, then $r \\in \\mathrm{spectrum}(B)$.$$

Lean4

/-- The roots of the characteristic polynomial are in the spectrum of the matrix. -/
theorem mem_spectrum_of_isRoot_charpoly [Nontrivial R] {r : R} (hr : IsRoot B.charpoly r) : r ∈ spectrum R B := by
  simp_all [eval_charpoly, spectrum.mem_iff, isUnit_iff_isUnit_det, algebraMap_eq_diagonal, Pi.algebraMap_def]

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