English
A group G is nilpotent if and only if its lower central series eventually reaches the trivial subgroup ⊥.
Русский
Группа G нильпотентна тогда и только тогда, когда нижняя центральная серия достигает тривиальной подгруппы ⊥ для некоторого конца.
LaTeX
$$$IsNilpotent G \\iff \\exists n, \\lowerCentralSeries G n = \\bot$$$
Lean4
/-- A group is nilpotent if and only if its lower central series eventually reaches
the trivial subgroup. -/
theorem nilpotent_iff_lowerCentralSeries : IsNilpotent G ↔ ∃ n, lowerCentralSeries G n = ⊥ :=
by
rw [nilpotent_iff_finite_descending_central_series]
constructor
· rintro ⟨n, H, ⟨h0, hs⟩, hn⟩
use n
rw [eq_bot_iff, ← hn]
exact descending_central_series_ge_lower H ⟨h0, hs⟩ n
· rintro ⟨n, hn⟩
exact ⟨n, lowerCentralSeries G, lowerCentralSeries_isDescendingCentralSeries, hn⟩
