Eigenvectors and eigenvalues over algebraically closed fields. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
- Every linear operator on a vector space over an algebraically closed field has an eigenvalue.
- The generalized eigenvectors span the entire vector space.
References #
Tags #
eigenspace, eigenvector, eigenvalue, eigen
theorem
module.End.exists_eigenvalue
{K : Type v}
{V : Type w}
[field K]
[add_comm_group V]
[module K V]
[is_alg_closed K]
[finite_dimensional K V]
[nontrivial V]
(f : module.End K V) :
∃ (c : K), f.has_eigenvalue c
Every linear operator on a vector space over an algebraically closed field has an eigenvalue.
@[protected, instance]
noncomputable
def
module.End.eigenvalues.inhabited
{K : Type v}
{V : Type w}
[field K]
[add_comm_group V]
[module K V]
[is_alg_closed K]
[finite_dimensional K V]
[nontrivial V]
(f : module.End K V) :
theorem
module.End.supr_generalized_eigenspace_eq_top
{K : Type v}
{V : Type w}
[field K]
[add_comm_group V]
[module K V]
[is_alg_closed K]
[finite_dimensional K V]
(f : module.End K V) :
The generalized eigenvectors span the entire vector space (Lemma 8.21 of [Axl15]).