Number_of_Powers_of_Cyclic_Group_Element
Provedcyclicgroup-theoryorderproofwiki
Let G be a cyclic group of order n generated by g. If d divides n, then g^(n/d) has exactly d distinct powers.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Number_of_Powers_of_Cyclic_Group_Element {G : Type _} [Group G] [Fintype G] (g : G) (hgen : Subgroup.zpowers g = ⊤) (d : ℕ) (hd : d ∣ Fintype.card G) (hd0 : 0 < d) : orderOf (g ^ (Fintype.card G / d)) = d := by sorrySource