to_quotient — Mathlib

English

If G is a p-group, then any quotient G/N by a normal subgroup N is also a p-group.

Русский

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

LaTeX

$$$\IsPGroup(p,G) \rightarrow \forall (H : Subgroup G) [H.Normal], \IsPGroup(p, G/\!H)$$$

Lean4

theorem to_quotient (H : Subgroup G) [H.Normal] : IsPGroup p (G ⧸ H) :=
  hG.of_surjective (QuotientGroup.mk' H) Quotient.mk''_surjective

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