n : ℕ
A : Type ?u.322503
R : Type ?u.322506
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_1
inst✝ : Group α
a : α
this :
  Nat.card ↑(MulAction.orbit { x // x ∈ zpowers a } 1) =
    Nat.card (ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) a) 1))
⊢ orderOf a = Nat.card { x // x ∈ zpowers a }
n : ℕ
A : Type ?u.322503
R : Type ?u.322506
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_1
inst✝ : Group α
a : α
⊢ orderOf a = Nat.card { x // x ∈ zpowers a }
have := Nat.card_congr (MulAction.orbitZpowersEquiv a (1 : α))
no goals
n : ℕ
A : Type ?u.322503
R : Type ?u.322506
inst✝² : AddGroup A
inst✝¹ : Ring R
α : Type u_1
inst✝ : Group α
a : α
this :
  Nat.card ↑(MulAction.orbit { x // x ∈ zpowers a } 1) =
    Nat.card (ZMod (Function.minimalPeriod ((fun x x_1 => x • x_1) a) 1))
⊢ orderOf a = Nat.card { x // x ∈ zpowers a }
rwa [Nat.card_zmod, orbit_subgroup_one_eq_self, eq_comm] at this