Cyclic_Group_Elements_whose_Powers_equal_Identity_v3
Provedcyclicgroup-theoryorderproofwiki
In a cyclic group of order n, if d divides n, then there are exactly d elements x with x^d = 1.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Cyclic_Group_Elements_whose_Powers_equal_Identity_v3 {G : Type _} [Group G] [Fintype G] [IsCyclic G] [DecidableEq G] (d : ℕ) (hd : d ∣ Fintype.card G) (hd0 : 0 < d) : Finset.card (Finset.univ.filter (fun x : G => x ^ d = 1)) = d := by sorrySource