Order_of_Element_in_Quotient_Group
Provedgroup-theoryorderproofwikiquotient-group
The order of aH in the quotient group G/H divides the order of a in G.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Element_in_Quotient_Group {G : Type _} [Group G] (H : Subgroup G) [H.Normal] (a : G) : orderOf (QuotientGroup.mk' H a) ∣ orderOf a := by sorrySource