Quotient_Group_of_Cyclic_Group
Provedcyclicgroup-theoryproofwikiquotient-group
If G is a cyclic group generated by g and H is a subgroup, then the coset gH generates the quotient group G/H.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Quotient_Group_of_Cyclic_Group {G : Type _} [Group G] (g : G) (hgen : Subgroup.zpowers g = ⊤) (H : Subgroup G) [H.Normal] : Subgroup.zpowers (QuotientGroup.mk' H g) = ⊤ := by sorrySource