instQuotientSubgroupOfFinite — Mathlib

English

If G is finite, and G is a Z-group, then G/H is a Z-group for any normal H ≤ G.

Русский

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

LaTeX

$$\( \text{If } G \text{ is finite and } G \text{ is a } Z\text{-group, and } H \lhd G, \ G/H \text{ is a } Z\text{-group}.$$

Lean4

instance [Finite G] [IsZGroup G] (H : Subgroup G) [H.Normal] : IsZGroup (G ⧸ H) :=
  of_surjective (QuotientGroup.mk'_surjective H)

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