English
In Noetherian context, the maximal generalized eigenspace equals the k-th generalized eigenspace at the index given by maxGenEigenspaceIndex.
Русский
В теории Нэттерийских модулей максимум обобщённого эйгенпространства совпадает с k-м обобщённым эйгенпространством на индексе maxGenEigenspaceIndex.
LaTeX
$$$\\maxGenEigenspace(f, \\mu) = \\mathrm{genEigenspace}(f, \\mu, \\mathrm{maxGenEigenspaceIndex}(f, \\mu)).$$$
Lean4
/-- For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel
`(f - μ • id) ^ k` for some `k`. -/
theorem maxGenEigenspace_eq [IsNoetherian R M] (f : End R M) (μ : R) :
maxGenEigenspace f μ = f.genEigenspace μ (maxGenEigenspaceIndex f μ) :=
genEigenspace_top_eq_maxUnifEigenspaceIndex _ _
