English
For a finite-dimensional module, an eigenvalue μ of f satisfies that μ is a root of the characteristic polynomial of f, and conversely.
Русский
Для конечномерного пространства собственное значение μ удовлетворяет тому, что μ является корнем характеристического многочлена f, и наоборот.
LaTeX
$$$f.HasEigenvalue(μ) \\iff (\\mathrm{charpoly}(f)).IsRoot(μ)$$$
Lean4
/-- The roots of the characteristic polynomial are exactly the eigenvalues.
`R` is required to be an integral domain, otherwise there is the counterexample:
R = M = Z/6Z, f(x) = 2x, v = 3, μ = 4, but p = X - 2.
-/
theorem hasEigenvalue_iff_isRoot_charpoly (f : End R M) (μ : R) : f.HasEigenvalue μ ↔ f.charpoly.IsRoot μ :=
by
rw [hasEigenvalue_iff, eigenspace_def, ← det_eq_zero_iff_ker_ne_bot, det_eq_sign_charpoly_coeff]
simp [Polynomial.coeff_zero_eq_eval_zero, charpoly_sub_smul]
