pow_mod_card_support_cycleOf_self_apply

English

If f x ≠ x, then (g^m) x = (g^n) x holds exactly when m mod |cycleOf x| = n mod |cycleOf x|.

Русский

Если f x ≠ x, тогда (g^m) x = (g^n) x эквивалентно m mod |cycleOf x| = n mod |cycleOf x|.

LaTeX

$$$[DecidableEq α] [Fintype α] \\Rightarrow (g^m) x = (g^n) x \\iff m \\\\bmod #(g.cycleOf x).\\\\support = n \\\\bmod #(g.cycleOf x).\\\\support$$$

Lean4

theorem pow_mod_card_support_cycleOf_self_apply [DecidableEq α] [Fintype α] (f : Perm α) (n : ℕ) (x : α) :
    (f ^ (n % #(f.cycleOf x).support)) x = (f ^ n) x :=
  by
  by_cases hx : f x = x
  · rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]
  · rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf, pow_mod_orderOf]

Похожие утверждения