English
The nilpotency class equals the smallest n for which the descending central series reaches ⊥.
Русский
Класс нильпотентности равен наименьшему n, при котором нисходящая центральная серия достигает ⊥.
LaTeX
$$$\\min\\{ n \\in \\mathbb{N} \\mid lowerCentralSeries(G,n) = \\bot \\} = \\mathrm{Group.nilpotencyClass} G$$$
Lean4
/-- The nilpotency class of a nilpotent `G` is equal to the smallest `n` for which the descending
central series reaches `⊥` in its `n`-th term. -/
theorem least_descending_central_series_length_eq_nilpotencyClass :
Nat.find ((nilpotent_iff_finite_descending_central_series G).mp hG) = Group.nilpotencyClass G :=
by
rw [← least_ascending_central_series_length_eq_nilpotencyClass]
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
· rintro n ⟨H, ⟨hH, hn⟩⟩
refine ⟨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 ⟨fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
dsimp only
rw [tsub_self]
exact hH.1
