Eigenvalues are the roots of the characteristic polynomial. #
Tags #
eigenvalue, characteristic polynomial
theorem
Module.End.hasEigenvalue_iff_isRoot_charpoly
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[IsDomain R]
[AddCommGroup M]
[Module R M]
[Free R M]
[Module.Finite R M]
(f : End R M)
(μ : R)
:
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
Module.End.mem_spectrum_iff_isRoot_charpoly
{K : Type u_3}
{V : Type u_4}
[Field K]
[AddCommGroup V]
[Module K V]
[Module.Finite K V]
(f : End K V)
(μ : K)
: