nilpotent_quotient_of_nilpotent — Mathlib

English

If G is nilpotent, then any quotient G/H by a normal subgroup H is also nilpotent.

Русский

Если G нильпотентна, то всякая фактор-группа G/H по нормальной подгруппе H тоже нильпотентна.

LaTeX

$$$\\operatorname{IsNilpotent}(G) \\;\\Rightarrow\\; \\operatorname{IsNilpotent}(G/H) \\quad (H \\trianglelefteq G)$$$

Lean4

/-- A quotient of a nilpotent group is nilpotent -/
instance nilpotent_quotient_of_nilpotent (H : Subgroup G) [H.Normal] [_h : IsNilpotent G] : IsNilpotent (G ⧸ H) :=
  nilpotent_of_surjective (QuotientGroup.mk' H) QuotientGroup.mk_surjective

Похожие утверждения