cycleOf — Mathlib

English

The cycle of f at x behaves well with inversion: the inverse of cycleOf f x equals cycleOf f^{-1} x.

Русский

Цикл цикла f в точке x коммутирует с операцией взятия обратного: (cycleOf f x)^{-1} = cycleOf f^{-1} x.

LaTeX

$$$ (cycleOf f x)^{-1} = cycleOf f^{-1} x $$$

Lean4

/-- `f.cycleOf x` is the cycle of the permutation `f` to which `x` belongs. -/
def cycleOf (f : Perm α) [DecidableRel f.SameCycle] (x : α) : Perm α :=
  ofSubtype (subtypePerm f fun _ => sameCycle_apply_right : Perm { y // SameCycle f x y })

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