English
For any f,g ∈ Perm(Fin(n)), signAux(fg) = signAux(f)·signAux(g).
Русский
Для любых f,g ∈ Perm(Fin(n)) выполняется signAux(fg) = signAux(f)·signAux(g).
LaTeX
$$$\forall n,\forall f,g \in \mathrm{Perm}(\mathrm{Fin}(n)),\ signAux(f g) = signAux(f) \cdot signAux(g)$$$
Lean4
theorem signAux_mul {n : ℕ} (f g : Perm (Fin n)) : signAux (f * g) = signAux f * signAux g :=
by
rw [← signAux_inv g]
unfold signAux
rw [← prod_mul_distrib]
refine prod_nbij (signBijAux g) signBijAux_mem signBijAux_injOn signBijAux_surj ?_
rintro ⟨a, b⟩ hab
dsimp only [signBijAux]
rw [mul_apply, mul_apply]
rw [mem_finPairsLT] at hab
by_cases h : g b < g a
· rw [dif_pos h]
simp only [not_le_of_gt hab, mul_one, Perm.inv_apply_self, if_false]
· rw [dif_neg h, inv_apply_self, inv_apply_self, if_pos hab.le]
by_cases h₁ : f (g b) ≤ f (g a)
· have : f (g b) ≠ f (g a) := by
rw [Ne, f.injective.eq_iff, g.injective.eq_iff]
exact ne_of_lt hab
rw [if_pos h₁, if_neg (h₁.lt_of_ne this).not_ge]
rfl
· rw [if_neg h₁, if_pos (lt_of_not_ge h₁).le]
rfl
