English
Two integer powers of a permutation agree on x precisely when their exponents are congruent modulo the cycle length.
Русский
Две целочисленные степени перестановки совпадают на x тогда и только тогда, когда их степени конгруэнтны по модулю длины цикла.
LaTeX
$$$(g x ≠ x) \\\\Rightarrow (g^m) x = (g^n) x \\\\iff m \\\\equiv n \\\\bmod #(g.cycleOf x).\\\\support$$$
Lean4
theorem zpow_eq_zpow_on_iff [DecidableEq α] [Fintype α] (g : Perm α) {m n : ℤ} {x : α} (hx : g x ≠ x) :
(g ^ m) x = (g ^ n) x ↔ m % #(g.cycleOf x).support = n % #(g.cycleOf x).support :=
by
rw [Int.emod_eq_emod_iff_emod_sub_eq_zero]
conv_lhs => rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]
simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]
rw [← Int.dvd_iff_emod_eq_zero]
rw [← cycleOf_zpow_apply_self g x, cycle_zpow_mem_support_iff]
· rw [← Int.dvd_iff_emod_eq_zero]
· exact isCycle_cycleOf g hx
· simp only [cycleOf_apply_self]; exact hx
