no goals
n : ℕ
A : Type ?u.315283
R : Type ?u.315286
inst✝⁴ : AddGroup A
inst✝³ : Ring R
α : Type u_2
β : Type u_1
inst✝² : Group α
a : α
inst✝¹ : MulAction α β
b : β
inst✝ : Fintype ↑(orbit { x // x ∈ zpowers a } b)
⊢ minimalPeriod ((fun x x_1 => x • x_1) a) b = Fintype.card ↑(orbit { x // x ∈ zpowers a } b)
rw [← Fintype.ofEquiv_card (orbitZpowersEquiv a b), @ZMod.card _ (_)]