English
For a permutation σ of Fin n, the sign equals the product over all i of the product over j in Iio(i) of whether σ(i) < σ(j) or not.
Русский
Для перестановки σ на Fin n знак равен произведению по всем i и по всем j ∈ Iio(i) индикатора отношения σ(i) < σ(j).
LaTeX
$$$\\forall {n : \\mathbb{N}} (\\sigma : \\mathrm{Equiv.Perm}(\\mathrm{Fin}(n))) :\\; \\sigma.\\mathrm{sign} = \\prod_{j} \\prod_{i \\in \\mathrm{Iio}(j)} \\text{(if } \\sigma(i) < \\sigma(j) \\text{ then } 1 \\text{ else } -1)$$$
Lean4
theorem sign_eq_prod_prod_Iio (σ : Equiv.Perm (Fin n)) :
σ.sign = ∏ j, ∏ i ∈ Finset.Iio j, (if σ i < σ j then 1 else -1) :=
by
suffices h : σ.sign = σ.signAux by
rw [h, Finset.prod_sigma', Equiv.Perm.signAux]
convert rfl using 2 with x hx
· simp [Finset.ext_iff, Equiv.Perm.mem_finPairsLT]
simp [← ite_not (p := _ ≤ _)]
refine σ.swap_induction_on (by simp) fun π i j hne h_eq ↦ ?_
rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne, Equiv.Perm.signAux_swap hne]
