cycleOf_one — Mathlib

English

The exponent reduction modulo the order of the cycleOf f x preserves the action on x: (f^(n mod orderOf (cycleOf f x))) x = f^n x.

Русский

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

LaTeX

$$(f ^ (n % orderOf (cycleOf f x))) x = (f ^ n) x$$

Lean4

theorem cycleOf_one [DecidableRel (1 : Perm α).SameCycle] (x : α) : cycleOf 1 x = 1 :=
  (cycleOf_eq_one_iff 1).mpr rfl

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