cycleOf_apply_apply_zpow_self — Mathlib

English

The order of the cycle of f at x controls the modulo reduction of exponents: f^{n mod orderOf (cycleOf f x)} applied to x equals f^n applied to x.

Русский

Порядок цикла cycleOf f x управляет редукцией показателей степени: f^{n mod orderOf (cycleOf f x)}(x) = f^n(x).

LaTeX

$$$ (f^{(n \\\\% \\\\ orderOf (cycleOf f x))}) x = (f^n) x $$$

Lean4

@[simp]
theorem cycleOf_apply_apply_zpow_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) (k : ℤ) :
    cycleOf f x ((f ^ k) x) = (f ^ (k + 1) : Perm α) x :=
  by
  rw [SameCycle.cycleOf_apply]
  · rw [add_comm, zpow_add, zpow_one, mul_apply]
  · exact ⟨k, rfl⟩

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