Power_of_Generator_of_Cyclic_Group_is_Generator_iff_Coprime
Provedcoprimecyclicgeneratorsgroup-theoryproofwiki
In a cyclic group C_n = <a>, C_n = <a^k> if and only if k is coprime with n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Power_of_Generator_of_Cyclic_Group_is_Generator_iff_Coprime {G : Type _} [Group G] [Fintype G] (a : G) (ha : Subgroup.zpowers a = ⊤) (k : ℤ) : Subgroup.zpowers (a ^ k) = ⊤ ↔ Int.gcd k (Fintype.card G) = 1 := by sorrySource