English
The nilpotency class of a quotient is at most the nilpotency class of the original group: for H ◁ G, nilpotencyClass(G/H) ≤ nilpotencyClass(G).
Русский
Класс нильпотентности фактор-группы не превосходит класса нильпотентности исходной группы: для H ◁ G выполняется nilpotencyClass(G/H) ≤ nilpotencyClass(G).
LaTeX
$$$\\operatorname{nilpotencyClass}(G/H) \\le \\operatorname{nilpotencyClass}(G)$$$
Lean4
/-- The nilpotency class of a quotient of `G` is less or equal the nilpotency class of `G` -/
theorem nilpotencyClass_quotient_le (H : Subgroup G) [H.Normal] [_h : IsNilpotent G] :
Group.nilpotencyClass (G ⧸ H) ≤ Group.nilpotencyClass G :=
nilpotencyClass_le_of_surjective (QuotientGroup.mk' H) QuotientGroup.mk_surjective
