Order_of_Subgroup_of_Cyclic_Group
Provedcyclicgroup-theoryorderproofwiki
Let C_n = <g> be a cyclic group of order n. Then for a = g^i, the order of a is n / gcd(n, i).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Subgroup_of_Cyclic_Group {G : Type _} [Group G] [Fintype G] (g : G) (hgen : Subgroup.zpowers g = ⊤) (i : ℕ) : orderOf (g ^ i) = Fintype.card G / Nat.gcd (Fintype.card G) i := by sorrySource