Quotient_Group_of_Infinite_Cyclic_Group_by_Subgroup
Provedcyclic-groupsgroup-theoryproofwikiquotient-groups
Let be the cyclic group of order . Then where is the additive group of integers is the additive group of integer multiples is the quotient group of by . Thus, every cyclic group is isomorphic to one of
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.RingTheory.Ideal.Quotient.Basic
Formal statement
theorem Quotient_Group_of_Infinite_Cyclic_Group_by_Subgroup (n : ℕ) (hn : 0 < n) : Nonempty (ZMod n ≃+* ℤ ⧸ Ideal.span ({(n : ℤ)} : Set ℤ)) := by sorrySource