English
For any n and f ∈ Perm(Fin(n)), signAux⁻¹ f = signAux f; i.e., signAux is invariant under taking inverses of f.
Русский
Для любого n и f ∈ Perm(Fin(n)) выполняется signAux(f⁻¹) = signAux(f); то есть знак сохраняется при взятии обратной перестановки.
LaTeX
$$$\forall n, \forall f \in \mathrm{Perm}(\mathrm{Fin}(n)),\ signAux(f^{-1}) = signAux(f)$$$
Lean4
@[simp]
theorem signAux_inv {n : ℕ} (f : Perm (Fin n)) : signAux f⁻¹ = signAux f :=
prod_nbij (signBijAux f⁻¹) signBijAux_mem signBijAux_injOn signBijAux_surj fun ⟨a, b⟩ hab ↦
if h : f⁻¹ b < f⁻¹ a then by
simp_all [signBijAux, if_neg h.not_ge, apply_inv_self, apply_inv_self, if_neg (mem_finPairsLT.1 hab).not_ge]
else by simp_all [signBijAux, dif_neg h, apply_inv_self, apply_inv_self, if_pos (mem_finPairsLT.1 hab).le]
