English
The nilpotency class equals the least n for which the ascending central series reaches G (reiterated).
Русский
Класс нильпотентности равен наименьшему n, при котором восходящая центральная серия достигает G (повторение объясняет повторение ранее).
LaTeX
$$$\\min\\{ n \\in \\mathbb{N} \\mid upperCentralSeries(G,n) = G \\} = \\mathrm{Group.nilpotencyClass} G$$$
Lean4
theorem map {H : Type*} [Group H] (f : G →* H) (n : ℕ) :
Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries H n := by
induction n with
| zero => simp
| succ d hd =>
rintro a ⟨x, hx : x ∈ lowerCentralSeries G d.succ, rfl⟩
refine
closure_induction (hx := hx) ?_ (by simp [f.map_one, Subgroup.one_mem _])
(fun y z _ _ hy hz => by simp [MonoidHom.map_mul, Subgroup.mul_mem _ hy hz])
(fun y _ hy => by rw [f.map_inv]; exact Subgroup.inv_mem _ hy)
rintro a ⟨y, hy, z, ⟨-, rfl⟩⟩
apply mem_closure.mpr
exact fun K hK => hK ⟨f y, hd (mem_map_of_mem f hy), by simp [commutatorElement_def]⟩
