Epimorphism_from_Integers_to_Cyclic_Group
Provedcyclicepimorphismgroup-theoryproofwiki
If G = <a> is a cyclic group generated by a, then the map f: Z -> G defined by f(n) = a^n is surjective (an epimorphism).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Epimorphism_from_Integers_to_Cyclic_Group {G : Type _} [Group G] (a : G) (hgen : Subgroup.zpowers a = ⊤) : Function.Surjective (fun n : ℤ => a ^ n) := by sorrySource