English
G is nilpotent iff there exists a finite ascending central series terminating at G.
Русский
G нильпотентна тогда и только тогда, когда существует конечная восходящая центральная серия, достигающая G.
LaTeX
$$$\text{IsNilpotent}(G) \iff \exists n:\mathbb{N},\exists H:\mathbb{N}\to\mathrm{Subgroup}(G),\ IsAscendingCentralSeries(H) \land H(n)=\top$$$
Lean4
/-- A group `G` is nilpotent iff there exists a descending central series which reaches the
trivial group in a finite time. -/
theorem nilpotent_iff_finite_descending_central_series :
IsNilpotent G ↔ ∃ n : ℕ, ∃ H : ℕ → Subgroup G, IsDescendingCentralSeries H ∧ H n = ⊥ :=
by
rw [nilpotent_iff_finite_ascending_central_series]
constructor
· rintro ⟨n, H, hH, hn⟩
refine ⟨n, fun m => H (n - m), is_descending_rev_series_of_is_ascending G hn hH, ?_⟩
dsimp only
rw [tsub_self]
exact hH.1
· rintro ⟨n, H, hH, hn⟩
refine ⟨n, fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
dsimp only
rw [tsub_self]
exact hH.1
