of_surjective — Mathlib

English

If G is a Z-group and f: G → G' is surjective, then G' is a Z-group.

Русский

Если G — Z-группа и f: G → G' сюръективен, то G' — Z-группа.

LaTeX

$$\( \text{If } G \text{ is a } Z\text{-group and } f: G \to G' \text{ is surjective, then } G' \text{ is a } Z\text{-group}.$$

Lean4

theorem of_surjective [Finite G] [hG : IsZGroup G] (hf : Function.Surjective f) : IsZGroup G' :=
  by
  rw [isZGroup_iff] at hG ⊢
  intro p hp P
  have := Fact.mk hp
  obtain ⟨Q, rfl⟩ := Sylow.mapSurjective_surjective hf p P
  specialize hG p hp Q
  exact isCyclic_of_surjective _ (f.subgroupMap_surjective Q)

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