isCyclic_of_surjective — Mathlib

English

If there is a surjective homomorphism f : F → G' and G' is cyclic, then G is cyclic.

Русский

Если существет сюръективный гомоморфизм f: F → G' и G' циклична, то G циклична.

LaTeX

$$$f : F \to G', \text{ surjective}, IsCyclic(G') \Rightarrow IsCyclic(G)$$$

Lean4

@[to_additive]
theorem isCyclic_of_surjective {F : Type*} [hH : IsCyclic G'] [FunLike F G' G] [MonoidHomClass F G' G] (f : F)
    (hf : Function.Surjective f) : IsCyclic G := by
  obtain ⟨x, hx⟩ := hH
  refine ⟨f x, fun a ↦ ?_⟩
  obtain ⟨a, rfl⟩ := hf a
  obtain ⟨n, rfl⟩ := hx a
  exact ⟨n, (map_zpow _ _ _).symm⟩

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