English
For any n and x ≠ y in Fin(n), signAux_swap hxy = -1, i.e., a transposition changes the sign by -1.
Русский
Для любых n и x ≠ y из Fin(n) знак транспозиции равен -1: signAux_swap(hxy) = -1.
LaTeX
$$$\forall n, \forall x,y \in \mathrm{Fin}(n), x \neq y \to signAux\_swap(h_{xy}) = -1$$$
Lean4
theorem signAux_swap : ∀ {n : ℕ} {x y : Fin n} (_hxy : x ≠ y), signAux (swap x y) = -1
| 0, x, y => by intro; exact Fin.elim0 x
| 1, x, y => by
dsimp [signAux, swap, swapCore]
simp only [eq_iff_true_of_subsingleton, not_true, ite_true, le_refl, prod_const, IsEmpty.forall_iff]
| n + 2, x, y => fun hxy => by
have h2n : 2 ≤ n + 2 := by exact le_add_self
rw [← isConj_iff_eq, ← signAux_swap_zero_one h2n]
exact (MonoidHom.mk' signAux signAux_mul).map_isConj (isConj_swap hxy (by exact of_decide_eq_true rfl))
