English
The sign of a sum congruence permutation factorizes as the product of the signs of the summands.
Русский
Знак суммы конгруэнтных перестановок раскладывается как произведение знаков слагаемых.
LaTeX
$$$\\operatorname{sign}(\\mathrm{sumCongr}(\\sigma_a,\\sigma_b)) = \\operatorname{sign}(\\sigma_a) \\cdot \\operatorname{sign}(\\sigma_b)$$$
Lean4
@[simp]
theorem sign_sumCongr (σa : Perm α) (σb : Perm β) : sign (sumCongr σa σb) = sign σa * sign σb :=
by
suffices sign (sumCongr σa (1 : Perm β)) = sign σa ∧ sign (sumCongr (1 : Perm α) σb) = sign σb by
rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
constructor
·
induction σa using swap_induction_on with
| one => simp
| swap_mul σa' a₁ a₂ ha ih =>
rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one, sign_swap ha,
sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
·
induction σb using swap_induction_on with
| one => simp
| swap_mul σb' b₁ b₂ hb ih =>
rw [← one_mul (1 : Perm α), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_one_swap, sign_swap hb,
sign_swap (Sum.inr_injective.ne_iff.mpr hb)]
