English
Similarly, the sign equals the product over i of the product over j in Ioi(i) of the same indicator, showing symmetry between Iio and Ioi formulations.
Русский
Аналогично, знак равен произведению по i и по j ∈ Ioi(i) тех же индикаций, демонстрируя симметрию между формулировками Iio и Ioi.
LaTeX
$$$\\forall {n : \\mathbb{N}} (\\sigma : \\mathrm{Equiv.Perm}(\\mathrm{Fin}(n))) :\\; \\sigma.\\mathrm{sign} = \\prod_{i} \\prod_{j \\in \\mathrm{Ioi}(i)} (\\text{if } \\sigma(i) < \\sigma(j) \\text{ then } 1 \\text{ else } -1)$$$
Lean4
theorem sign_eq_prod_prod_Ioi (σ : Equiv.Perm (Fin n)) :
σ.sign = ∏ i, ∏ j ∈ Finset.Ioi i, (if σ i < σ j then 1 else -1) :=
by
rw [σ.sign_eq_prod_prod_Iio]
apply Finset.prod_comm' (by simp)
