pow_mod_orderOf_cycleOf_apply — Mathlib

English

For any n, (cycleOf f x)^n applied to x equals f^n x; this holds for natural powers.

Русский

Для любого n, (cycleOf f x)^n применяется к x так же, как f^n x.

LaTeX

$$cycleOf_pow_apply_self (f : Perm α) (x : α) (n : Nat) : (cycleOf f x ^ n) x = (f ^ n) x$$

Lean4

theorem pow_mod_orderOf_cycleOf_apply (f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) :
    (f ^ (n % orderOf (cycleOf f x))) x = (f ^ n) x := by
  rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]

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