English
Let f be an endomorphism of a finite-dimensional R-module M which is finitely semisimple. Then for every μ ∈ R and every k > 0 (k ∈ ENat), the generalized eigenspace f.genEigenspace μ k coincides with the ordinary eigenspace f.eigenspace μ.
Русский
Пусть f — конечномерное R-отображение модуля M, являющееся конечносемисимплефическим. Тогда для любого μ ∈ R и любого k > 0 (k ∈ ENat) обобщённое эйгенпространство f.genEigenspace μ k совпадает с обычным эйгенпространством f.eigenspace μ.
LaTeX
$$$f\\text{.genEigenspace }\\mu\\, k = f\\text{.eigenspace }\\mu\\quad(0 < k).$$$
Lean4
theorem genEigenspace_eq_eigenspace (hf : f.IsFinitelySemisimple) (μ : R) {k : ℕ∞} (hk : 0 < k) :
f.genEigenspace μ k = f.eigenspace μ :=
by
refine le_antisymm (fun m hm ↦ mem_eigenspace_iff.mpr ?_) (f.genEigenspace μ |>.mono ?_)
· apply apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil hm rfl hf
simp
· exact Order.one_le_iff_pos.mpr hk
