cycleOf_zpow_apply_self — Mathlib

English

There is a canonical equivalence between the cyclic permutations and the nontrivial nodup cycles as described by EquivPerm.isoCycle'.

Русский

Существует каноническое эквивалентное соответствие между циклическими перестановками и ненулевыми неповторяющимися циклами, заданное через EquivPerm.isoCycle'.

LaTeX

$$$\\text{isoCycle'} : \\{ f : Perm α \\mid IsCycle f \\} \\simeq \\{ s : Cycle α \\mid s.Nodup \\land s.Nontrivial \\}$$$

Lean4

@[simp]
theorem cycleOf_zpow_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
    ∀ n : ℤ, (cycleOf f x ^ n) x = (f ^ n) x := by
  intro z
  cases z with
  | ofNat z => exact cycleOf_pow_apply_self f x z
  | negSucc z => rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]

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