English
For any lists l1 and l2 in a commutative group, the alternatingProd of their concatenation satisfies a multiplicative relation with the alternatingProds of the parts: alternatingProd(l1 ++ l2) = alternatingProd(l1) · (alternatingProd(l2))^{(-1)^{|l1|}}.
Русский
Для любых списков l1 и l2 в коммутативной группе чередующее произведение от их конкатенации равно произведению чередующего произведения l1 на чередующее произведение l2 в степени (-1)^{|l1|}.
LaTeX
$$$$ \operatorname{alternatingProd}(l_1 \++\ l_2) = \operatorname{alternatingProd}(l_1) \cdot (\operatorname{alternatingProd}(l_2))^{(-1)^{|l_1|}}. $$$$
Lean4
@[to_additive]
theorem alternatingProd_append :
∀ l₁ l₂ : List G, alternatingProd (l₁ ++ l₂) = alternatingProd l₁ * alternatingProd l₂ ^ (-1 : ℤ) ^ length l₁
| [], l₂ => by simp
| a :: l₁, l₂ => by
simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ', Int.neg_mul, one_mul,
zpow_neg, ← div_eq_mul_inv, div_div]
