no goals
α : Type u_2
β : Type u_1
inst✝¹ : Group α
inst✝ : MulAction α β
a : α
b : β
n : ℕ
⊢ a ^ n • b = b ↔ minimalPeriod ((fun x x_1 => x • x_1) a) b ∣ n
rw [← isPeriodicPt_iff_minimalPeriod_dvd, IsPeriodicPt, IsFixedPt, smul_iterate]