English
If f: G → G' is an injective homomorphism and G' is a Z-group, then G is a Z-group.
Русский
Если существует инъективное гомоморфизм f: G → G' и G' - Z-группа, то и G - Z-группа.
LaTeX
$$\( \text{If } f: G \to G' \text{ is injective and } G' \text{ is a } Z\text{-group, then } G \text{ is a } Z\text{-group}.$$
Lean4
theorem of_injective [hG' : IsZGroup G'] (hf : Function.Injective f) : IsZGroup G :=
by
rw [isZGroup_iff] at hG' ⊢
intro p hp P
obtain ⟨Q, hQ⟩ := P.exists_comap_eq_of_injective hf
specialize hG' p hp Q
have h : Subgroup.map f P ≤ Q := hQ ▸ Subgroup.map_comap_le f ↑Q
have := isCyclic_of_surjective _ (Subgroup.subgroupOfEquivOfLe h).surjective
exact isCyclic_of_surjective _ (Subgroup.equivMapOfInjective P f hf).symm.surjective
