Eigenvalues are the roots of the minimal polynomial. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Tags #
eigenvalue, minimal polynomial
theorem
module.End.eigenspace_aeval_polynomial_degree_1
{K : Type v}
{V : Type w}
[field K]
[add_comm_group V]
[module K V]
(f : module.End K V)
(q : polynomial K)
(hq : q.degree = 1) :
f.eigenspace (-q.coeff 0 / q.leading_coeff) = linear_map.ker (⇑(polynomial.aeval f) q)
theorem
module.End.ker_aeval_ring_hom'_unit_polynomial
{K : Type v}
{V : Type w}
[field K]
[add_comm_group V]
[module K V]
(f : module.End K V)
(c : (polynomial K)ˣ) :
linear_map.ker (⇑(polynomial.aeval f) ↑c) = ⊥
theorem
module.End.aeval_apply_of_has_eigenvector
{K : Type v}
{V : Type w}
[field K]
[add_comm_group V]
[module K V]
{f : module.End K V}
{p : polynomial K}
{μ : K}
{x : V}
(h : f.has_eigenvector μ x) :
⇑(⇑(polynomial.aeval f) p) x = polynomial.eval μ p • x
theorem
module.End.is_root_of_has_eigenvalue
{K : Type v}
{V : Type w}
[field K]
[add_comm_group V]
[module K V]
{f : module.End K V}
{μ : K}
(h : f.has_eigenvalue μ) :
theorem
module.End.has_eigenvalue_of_is_root
{K : Type v}
{V : Type w}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{f : module.End K V}
{μ : K}
(h : (minpoly K f).is_root μ) :
f.has_eigenvalue μ
theorem
module.End.has_eigenvalue_iff_is_root
{K : Type v}
{V : Type w}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{f : module.End K V}
{μ : K} :
f.has_eigenvalue μ ↔ (minpoly K f).is_root μ
@[protected, instance]
noncomputable
def
module.End.eigenvalues.fintype
{K : Type v}
{V : Type w}
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V]
(f : module.End K V) :
An endomorphism of a finite-dimensional vector space has finitely many eigenvalues.