symm_sign — Mathlib

English

The sign of the permutation decomposeFin.symm(p,e) equals sign(e) multiplied by (-1) if p ≠ 0 and by 1 if p = 0.

Русский

Знак перестановки decomposeFin.symm(p,e) равен знаку e умноженному на (-1), если p ≠ 0, и на 1, если p = 0.

LaTeX

$$$ \\operatorname{sign}(\\mathrm{decomposeFin.symm}(p,e)) = \\begin{cases} \\operatorname{sign}(e), & p=0 \\\\ -\\operatorname{sign}(e), & p\\neq 0 \\end{cases}$$$

Lean4

@[simp]
theorem symm_sign {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) :
    Perm.sign (Equiv.Perm.decomposeFin.symm (p, e)) = ite (p = 0) 1 (-1) * Perm.sign e := by
  refine Fin.cases ?_ ?_ p <;> simp [Equiv.Perm.decomposeFin]

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