English
For a permutation on Fin n, signAux computes its sign as the product over all pairs (x1,x2) with x2 < x1 of −1 if the permutation preserves the order, and +1 otherwise.
Русский
Для перестановки на Fin n signAux вычисляет знак как произведение по всем парам (x1,x2) с x2 < x1: −1 если перестановка сохраняет порядок, иначе +1.
LaTeX
$$$ \\text{signAux}(\\sigma) = \\prod_{x \\in \\mathrm{finPairsLT}\\ n} \\begin{cases} -1, & \\sigma x.1 \\le \\sigma x.2 \\\\ 1, & \\text{иначе} \\end{cases} $$$
Lean4
/-- `signAux σ` is the sign of a permutation on `Fin n`, defined as the parity of the number of
pairs `(x₁, x₂)` such that `x₂ < x₁` but `σ x₁ ≤ σ x₂` -/
def signAux {n : ℕ} (a : Perm (Fin n)) : ℤˣ :=
∏ x ∈ finPairsLT n, if a x.1 ≤ a x.2 then -1 else 1
