English
Let s be a finite multiset of a type with a commutative semiring structure. Then the product of (f i + g i) over i ∈ s equals the sum over all antidiagonal decompositions of s of the product of f-values on the first component and g-values on the second component.
Русский
Пусть s — конечное мультимножество; произведение по i∈s (f(i) + g(i)) разлагается как сумма по всем разложениям типа antidiagonal: произведение f-значений на первом компоненте и произведение g-значений на втором компоненте.
LaTeX
$$$$ \\prod_{i \\in s} (f(i) + g(i)) = \\sum_{p \\in (\\operatorname{antidiagonal} s)} \\left( \\prod_{i \\in p.\\text{fst}} f(i) \\right) \\left( \\prod_{i \in p.\\text{snd}} g(i) \\right). $$$$
Lean4
theorem prod_map_add {s : Multiset ι} {f g : ι → R} :
prod (s.map fun i ↦ f i + g i) = sum ((antidiagonal s).map fun p ↦ (p.1.map f).prod * (p.2.map g).prod) :=
by
refine s.induction_on ?_ fun a s ih ↦ ?_
· simp only [map_zero, prod_zero, antidiagonal_zero, map_singleton, mul_one, sum_singleton]
· simp only [map_cons, prod_cons, ih, sum_map_mul_left.symm, add_mul, mul_left_comm (f a), mul_left_comm (g a),
sum_map_add, antidiagonal_cons, Prod.map_fst, Prod.map_snd, id_eq, map_add, map_map, Function.comp_apply,
mul_assoc, sum_add]
exact add_comm _ _
