# Eigenvalues are the roots of the minimal polynomial. #

## Tags #

eigenvalue, minimal polynomial

source
theorem Module.End.ker_aeval_ring_hom'_unit_polynomial {R : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : End R M) (c : (Polynomial R)ˣ) :
LinearMap.ker ((Polynomial.aeval f) ↑c) = ⊥
source
theorem Module.End.aeval_apply_of_hasEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} {p : Polynomial R} {μ : R} {x : M} (h : f.HasEigenvector μ x) :
((Polynomial.aeval f) p) x = Polynomial.eval μ p • x
source
theorem Module.End.isRoot_of_hasEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {f : End R M} {μ : R} (h : f.HasEigenvalue μ) :
(minpoly R f).IsRoot μ
source
theorem Module.End.hasEigenvalue_of_isRoot {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} {μ : R} [IsDomain R] [Module.Finite R M] (h : (minpoly R f).IsRoot μ) :
f.HasEigenvalue μ
source
theorem Module.End.hasEigenvalue_iff_isRoot {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} {μ : R} [IsDomain R] [Module.Finite R M] [NoZeroSMulDivisors R M] :
f.HasEigenvalue μ ↔ (minpoly R f).IsRoot μ
source
theorem Module.End.finite_hasEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : End R M) [IsDomain R] [Module.Finite R M] [NoZeroSMulDivisors R M] :
Set.Finite f.HasEigenvalue
source
noncomputable instance Module.End.instFintypeEigenvalues {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : End R M) [IsDomain R] [Module.Finite R M] [NoZeroSMulDivisors R M] :
Fintype f.Eigenvalues

An endomorphism of a finite-dimensional vector space has finitely many eigenvalues.

Equations

- f.instFintypeEigenvalues = ⋯.fintype

source
theorem Module.End.eigenspace_aeval_polynomial_degree_1 {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] (f : End K V) (q : Polynomial K) (hq : q.degree = 1) :
f.eigenspace (-q.coeff 0 / q.leadingCoeff) = LinearMap.ker ((Polynomial.aeval f) q)
source
theorem Module.End.finite_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) :
(spectrum K f).Finite

An endomorphism of a finite-dimensional vector space has a finite spectrum.

source
theorem Matrix.finite_spectrum {n : Type u_1} {R : Type u_2} [Field R] [Fintype n] [DecidableEq n] (A : Matrix n n R) :
(spectrum R A).Finite

An n x n matrix over a field has a finite spectrum.

source
instance Matrix.instFiniteSpectrum {n : Type u_1} {R : Type u_2} [Field R] [Fintype n] [DecidableEq n] (A : Matrix n n R) :
Finite ↑(spectrum R A)