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) μ)
:
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)
:
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)
:
An endomorphism of a finite-dimensional vector space has finitely many eigenvalues.