instDecidableRelSameCycleInv — Mathlib

English

If f is a permutation, there is a decidable relation for the inverse SameCycle relation, determined by f.

Русский

Если f — перестановка, существует разрешимое (решаемое) отношение для обратной операции SameCycle, зависящее от f.

LaTeX

$$$\\text{instance }(f:\\mathrm{Perm}(\\alpha))\\ [DecidableRel (f.SameCycle^{-1})] : DecidableRel (f^{-1}.SameCycle).$$$

Lean4

instance (f : Perm α) [DecidableRel (SameCycle f)] : DecidableRel (SameCycle f⁻¹) := fun x y =>
  decidable_of_iff (f.SameCycle x y) (sameCycle_inv).symm

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