English
For a finite set s and a cycle g, the zpow of g on s respects the order of the cycle within its support.
Русский
Для цикла g и ограниченного множества s порядок действия внутри опоры сохраняется в zpow.
LaTeX
$$$g^{n} x = x \\iff n \\equiv 0 \\pmod{|g|}$ для x в опоре$$
Lean4
theorem cycle_zpow_mem_support_iff {g : Perm α} (hg : g.IsCycle) {n : ℤ} {x : α} (hx : g x ≠ x) :
(g ^ n) x = x ↔ n % #g.support = 0 := by
set q := n / #g.support
set r := n % #g.support
have div_euc : r + #g.support * q = n ∧ 0 ≤ r ∧ r < #g.support :=
by
rw [← Int.ediv_emod_unique _]
· exact ⟨rfl, rfl⟩
simp only [Int.natCast_pos]
apply lt_of_lt_of_le _ (IsCycle.two_le_card_support hg); simp
simp only [← hg.orderOf] at div_euc
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le div_euc.2.1
simp only [hm, Nat.cast_nonneg, Nat.cast_lt, true_and] at div_euc
rw [← div_euc.1, zpow_add g]
simp only [hm, Nat.cast_eq_zero, zpow_natCast, coe_mul, comp_apply, zpow_mul, pow_orderOf_eq_one, one_zpow, coe_one,
id_eq]
have : (g ^ m) x = x ↔ g ^ m = 1 := by
constructor
· intro hgm
simp only [IsCycle.pow_eq_one_iff hg]
use x
· intro hgm
simp only [hgm, coe_one, id_eq]
rw [this]
by_cases hm0 : m = 0
· simp only [hm0, pow_zero]
· simp only [hm0, iff_false]
exact pow_ne_one_of_lt_orderOf hm0 div_euc.2
