English
Let R be a commutative semiring. For a multiset s of multisets of R, the product of the sums of the inner multisets equals the sum over all sections of s of the product of the inner products: ∏_{T∈s} (∑_{x∈T} x) = ∑_{S∈Sections(s)} ∏_{T∈S} (∏_{x∈T} x).
Русский
Пусть R — коммутативная полусистема. Если s является мультимножество мультимножеств R, то произведение сумм внутренних мультимножеств равно сумме по всем секциям s произведений внутренних произведений.
LaTeX
$$$$ \prod_{T \in s} \left( \sum_{x \in T} x \right) = \sum_{S \in \operatorname{Sections}(s)} \prod_{T \in S} \left( \prod_{x \in T} x \right). $$$$
Lean4
theorem prod_map_sum {s : Multiset (Multiset R)} : prod (s.map sum) = sum ((Sections s).map prod) :=
Multiset.induction_on s (by simp) fun a s ih ↦ by simp [ih, map_bind, sum_map_mul_left, sum_map_mul_right]
