English
Let f be an endomorphism of a finitely generated R-module M. Then f is nilpotent if and only if for every m ∈ M there exists n ∈ ℕ such that f^n(m) = 0.
Русский
Пусть f - эндоморфизм конечнопорождённого R-модуля M. Тогда f нильпотентен тогда и только тогда, когда для каждого элемента m ∈ M существует натуральное n such that f^n(m) = 0.
LaTeX
$$$\\text{IsNilpotent}(f) \\iff \\forall m \\in M, \\exists n \\in \\mathbb{N}, f^n(m) = 0.$$$
Lean4
theorem isNilpotent_iff_of_finite [Module.Finite R M] {f : End R M} : IsNilpotent f ↔ ∀ m : M, ∃ n : ℕ, (f ^ n) m = 0 :=
by
refine ⟨fun ⟨n, hn⟩ m ↦ ⟨n, by simp [hn]⟩, fun h ↦ ?_⟩
rcases Module.Finite.fg_top (R := R) (M := M) with ⟨S, hS⟩
choose g hg using h
use Finset.sup S g
ext m
have hm : m ∈ Submodule.span R S := by simp [hS]
induction hm using Submodule.span_induction with
| mem x hx => exact pow_map_zero_of_le (Finset.le_sup hx) (hg x)
| zero => simp
| add => simp_all
| smul => simp_all
