# Documentation

Mathlib.LinearAlgebra.Eigenspace.IsAlgClosed

# Eigenvectors and eigenvalues over algebraically closed fields. #

• Every linear operator on a vector space over an algebraically closed field has an eigenvalue.
• The generalized eigenvectors span the entire vector space.

## References #

• [Sheldon Axler, Linear Algebra Done Right][axler2015]
• https://en.wikipedia.org/wiki/Eigenvalues_and_eigenvectors

## Tags #

eigenspace, eigenvector, eigenvalue, eigen

theorem Module.End.exists_eigenvalue {K : Type v} {V : Type w} [] [] [Module K V] [] [] [] (f : ) :
c,

Every linear operator on a vector space over an algebraically closed field has an eigenvalue.

noncomputable instance Module.End.instInhabitedEigenvaluesToCommRingToEuclideanDomain {K : Type v} {V : Type w} [] [] [Module K V] [] [] [] (f : ) :
theorem Module.End.iSup_generalizedEigenspace_eq_top {K : Type v} {V : Type w} [] [] [Module K V] [] [] (f : ) :
⨆ (μ : K) (k : ), ↑() k =

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