English
In finite dimensions over an algebraically closed field, the generalized eigenspaces of any linear endomorphism span the whole space.
Русский
В конечномерном случае над алгебраически замкнутым полем обобщённые эйгенпространства линейного отображения заполняют всё пространство.
LaTeX
$$$\\bigvee_{\\mu} \\; f.maxGenEigenspace(\\mu) = ⊤$$$
Lean4
noncomputable instance [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : End K V) : Inhabited f.Eigenvalues :=
⟨⟨f.exists_eigenvalue.choose, f.exists_eigenvalue.choose_spec⟩⟩
-- Lemma 8.21 of [axler2015]
