ι : Type ?u.1728030
α : Type u_1
β : Type ?u.1728036
f g : Perm α
s✝ t : Set α
a b x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
m n : ℕ
⊢ ↑(f ^ m) a = ↑(f ^ n) a ↔ ↑(f ^ (↑n - ↑m)) a = a
ι : Type ?u.1728030
α : Type u_1
β : Type ?u.1728036
f g : Perm α
s✝ t : Set α
a b x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
m n : ℕ
⊢ ↑(f ^ m) a = ↑(f ^ n) a ↔ m ≡ n [MOD card s]
rw [Nat.modEq_iff_dvd, ← hf.zpow_apply_eq ha]
no goals
ι : Type ?u.1728030
α : Type u_1
β : Type ?u.1728036
f g : Perm α
s✝ t : Set α
a b x y : α
s : Finset α
hf : IsCycleOn f ↑s
ha : a ∈ s
m n : ℕ
⊢ ↑(f ^ m) a = ↑(f ^ n) a ↔ ↑(f ^ (↑n - ↑m)) a = a
simp [sub_eq_neg_add, zpow_add, eq_inv_iff_eq, eq_comm]