ι : Type ?u.1696537
α : Type u_1
β : Type ?u.1696543
f g : Perm α
s✝ t : Set α
a b x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℕ
⊢ ↑(f⁻¹ ^ (n + 1)) a = a ↔ ↑(card s) ∣ Int.negSucc n
ι : Type ?u.1696537
α : Type u_1
β : Type ?u.1696543
f g : Perm α
s✝ t : Set α
a b x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℕ
⊢ ↑(f ^ Int.negSucc n) a = a ↔ ↑(card s) ∣ Int.negSucc n
rw [zpow_negSucc, ← inv_pow]
no goals
ι : Type ?u.1696537
α : Type u_1
β : Type ?u.1696543
f g : Perm α
s✝ t : Set α
a b x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
n : ℕ
⊢ ↑(f⁻¹ ^ (n + 1)) a = a ↔ ↑(card s) ∣ Int.negSucc n
exact (hf.inv.pow_apply_eq ha).trans (dvd_neg.trans Int.coe_nat_dvd).symm