cycleOf_self_apply_zpow — Mathlib

English

The invariance of the cycle under integer powers: cycleOf f ((f^n) x) = cycleOf f x for all integers n.

Русский

Непропуск циклического разложения сохраняется при целочисленных степенях: cycleOf f ((f^n) x) = cycleOf f x для всех целых n.

LaTeX

$$cycleOf_self_apply_zpow (f : Perm α) (n : Int) (x : α) : cycleOf f ((f ^ n) x) = cycleOf f x$$

Lean4

@[simp]
theorem cycleOf_self_apply_zpow (f : Perm α) [DecidableRel f.SameCycle] (n : ℤ) (x : α) :
    cycleOf f ((f ^ n) x) = cycleOf f x :=
  SameCycle.rfl.zpow_left.cycleOf_eq

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