Eigenvalues are the roots of the minimal polynomial.

Tags

eigenvalue, minimal polynomial

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

theorem Module.End.ker_aeval_ring_hom'_unit_polynomial {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] (f : Module.End K V) (c : (Polynomial K)ˣ) : LinearMap.ker ((Polynomial.aeval f) ↑c) = ⊥

theorem Module.End.aeval_apply_of_hasEigenvector {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] {f : Module.End K V} {p : Polynomial K} {μ : K} {x : V} (h : Module.End.HasEigenvector f μ x) : ((Polynomial.aeval f) p) x = Polynomial.eval μ p • x

theorem Module.End.isRoot_of_hasEigenvalue {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] {f : Module.End K V} {μ : K} (h : Module.End.HasEigenvalue f μ) : Polynomial.IsRoot (minpoly K f) μ

theorem Module.End.hasEigenvalue_of_isRoot {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} (h : Polynomial.IsRoot (minpoly K f) μ) : Module.End.HasEigenvalue f μ

theorem Module.End.hasEigenvalue_iff_isRoot {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : Module.End.HasEigenvalue f μ ↔ Polynomial.IsRoot (minpoly K f) μ

theorem Module.End.finite_hasEigenvalue {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : Set.Finite (Module.End.HasEigenvalue f)

noncomputable instance Module.End.instFintypeEigenvaluesToCommRingToEuclideanDomain {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) : Fintype (Module.End.Eigenvalues f)

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

Equations

• Module.End.instFintypeEigenvaluesToCommRingToEuclideanDomain f = Set.Finite.fintype ⋯