English
signAux3 (f*g) hs = signAux3 f hs · signAux3 g hs and signAux3 (swap x y) hs = -1 for x ≠ y.
Русский
signAux3 (f g) hs = signAux3 f hs · signAux3 g hs и signAux3 (swap x y) hs = -1 при x ≠ y.
LaTeX
$$$\forall f,g, hs,\ signAux3(f g) hs = signAux3(f) hs \cdot signAux3(g) hs \quad\land\quad \forall x y, x \neq y,\ signAux3(swap x y) hs = -1$$$
Lean4
theorem signAux3_mul_and_swap [Finite α] (f g : Perm α) (s : Multiset α) (hs : ∀ x, x ∈ s) :
signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ Pairwise fun x y => signAux3 (swap x y) hs = -1 :=
by
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin α
induction s using Quotient.inductionOn with
| _ l => ?_
change signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ Pairwise fun x y => signAux2 l (swap x y) = -1
have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e :=
Equiv.ext fun h => by simp [mul_apply]
constructor
·
rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
signAux_eq_signAux2 _ _ e fun _ _ => hs _, hfg, signAux_mul]
· intro x y hxy
rw [← e.injective.ne_iff] at hxy
rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hxy]
