English
If f has eigenvalue μ and k > 0, then the generalized eigenspace f.genEigenspace μ k has positive finite dimension.
Русский
Если у f есть собственное значение μ и k > 0, то размерность обобщённого эйгенпространства f.genEigenspace μ k положительна и конечна.
LaTeX
$$$0 <\\mathrm{finrank}_K\\big( f.\\mathrm{genEigenspace}(μ,k)\\big)$$$
Lean4
/-- The generalized eigenspace of an eigenvalue has positive dimension for positive exponents. -/
theorem pos_finrank_genEigenspace_of_hasEigenvalue [FiniteDimensional K V] {f : End K V} {k : ℕ} {μ : K}
(hx : f.HasEigenvalue μ) (hk : 0 < k) : 0 < finrank K (f.genEigenspace μ k) :=
calc
0 = finrank K (⊥ : Submodule K V) := by rw [finrank_bot]
_ < finrank K (f.eigenspace μ) := (Submodule.finrank_lt_finrank_of_lt (bot_lt_iff_ne_bot.2 hx))
_ ≤ finrank K (f.genEigenspace μ k) :=
Submodule.finrank_mono ((f.genEigenspace μ).monotone (by simpa using Nat.succ_le_of_lt hk))
