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) : f.HasEigenvalue μ ↔ (LinearMap.charpoly f).IsRoot μ

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) : μ ∈ spectrum K f ↔ (LinearMap.charpoly f).IsRoot μ

theorem Module.End.det_eq_prod_roots_charpoly_of_splits {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] [Module.Finite K V] {f : End K V} (h : (LinearMap.charpoly f).Splits) : LinearMap.det f = (LinearMap.charpoly f).roots.prod

theorem Module.End.trace_eq_sum_roots_charpoly_of_splits {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] [Module.Finite K V] {f : End K V} (h : (LinearMap.charpoly f).Splits) : (LinearMap.trace K V) f = (LinearMap.charpoly f).roots.sum