decomposeOption_symm_sign — Mathlib

English

Taking the sign of the decomposed symmetric inverse equals the sign of the original permutation e.

Русский

Знак симметричной обратной операции декомпозиции равен знаку исходной перестановки e.

LaTeX

$$$ \\mathrm{sign}(\\mathrm{Equiv.Perm}.\\mathrm{decomposeOption}.\\mathrm{symm} (\\mathrm{none}, e)) = \\mathrm{sign}(e) $$$

Lean4

theorem decomposeOption_symm_sign {α : Type*} [DecidableEq α] [Fintype α] (e : Perm α) :
    Perm.sign (Equiv.Perm.decomposeOption.symm (none, e)) = Perm.sign e := by simp

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