English
For a finite-dimensional K-vector space V and f ∈ End_K(V), there exists k with k ≤ finrank_K(V) and ker(f^k) = ker(f^{k+1}).
Русский
Для конечномерного пространства V и эндоморфизма f существует k ≤ dim V such that ker(f^k) = ker(f^{k+1}).
LaTeX
$$$\\exists k \\le \\operatorname{finrank}_K V\\; (\\ker(f^k) = \\ker(f^{k+1}))$.$$
Lean4
theorem isSimpleOrder_of_finrank (hr : finrank F E = 2) : IsSimpleOrder (Subalgebra F E) :=
let i := nontrivial_of_finrank_pos (zero_lt_two.trans_eq hr.symm)
{ toNontrivial := ⟨⟨⊥, ⊤, fun h => by cases hr.symm.trans (Subalgebra.bot_eq_top_iff_finrank_eq_one.1 h)⟩⟩
eq_bot_or_eq_top := by
intro S
haveI : FiniteDimensional F E := .of_finrank_eq_succ hr
haveI : FiniteDimensional F S := FiniteDimensional.finiteDimensional_submodule (Subalgebra.toSubmodule S)
have : finrank F S ≤ 2 := hr ▸ S.toSubmodule.finrank_le
have : 0 < finrank F S := finrank_pos_iff.mpr inferInstance
interval_cases h : finrank F { x // x ∈ S }
· left
exact Subalgebra.eq_bot_of_finrank_one h
· right
rw [← hr] at h
rw [← Algebra.toSubmodule_eq_top]
exact eq_top_of_finrank_eq h }
