cycleOf_self_apply_pow — Mathlib

English

The cycle containing (f^n) x is the same as the cycle containing x for any n.

Русский

Цикл, содержащий (f^n) x, равен циклу, содержащему x, для любого n.

LaTeX

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

Lean4

@[simp]
theorem cycleOf_self_apply_pow (f : Perm α) [DecidableRel f.SameCycle] (n : ℕ) (x : α) :
    cycleOf f ((f ^ n) x) = cycleOf f x :=
  SameCycle.rfl.pow_left.cycleOf_eq

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