mathlib3 documentation


Eigenvectors and eigenvalues over algebraically closed fields. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

The generalized eigenvectors span the entire vector space (Lemma 8.21 of [Axl15]).