# 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} [] [] [Module K V] (f : ) (q : ) (hq : q.degree = 1) :
f.eigenspace (-q.coeff 0 / q.leadingCoeff) = LinearMap.ker (() q)
theorem Module.End.ker_aeval_ring_hom'_unit_polynomial {K : Type v} {V : Type w} [] [] [Module K V] (f : ) (c : ()ˣ) :
LinearMap.ker (() c) =
theorem Module.End.aeval_apply_of_hasEigenvector {K : Type v} {V : Type w} [] [] [Module K V] {f : } {p : } {μ : K} {x : V} (h : f.HasEigenvector μ x) :
(() p) x = x
theorem Module.End.isRoot_of_hasEigenvalue {K : Type v} {V : Type w} [] [] [Module K V] {f : } {μ : K} (h : f.HasEigenvalue μ) :
(minpoly K f).IsRoot μ
theorem Module.End.hasEigenvalue_of_isRoot {K : Type v} {V : Type w} [] [] [Module K V] [] {f : } {μ : K} (h : (minpoly K f).IsRoot μ) :
f.HasEigenvalue μ
theorem Module.End.hasEigenvalue_iff_isRoot {K : Type v} {V : Type w} [] [] [Module K V] [] {f : } {μ : K} :
f.HasEigenvalue μ (minpoly K f).IsRoot μ
theorem Module.End.finite_hasEigenvalue {K : Type v} {V : Type w} [] [] [Module K V] [] (f : ) :
Set.Finite f.HasEigenvalue
noncomputable instance Module.End.instFintypeEigenvalues {K : Type v} {V : Type w} [] [] [Module K V] [] (f : ) :
Fintype f.Eigenvalues

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

Equations
• f.instFintypeEigenvalues = .fintype