English
Let α be a CommMonoid. For any S ∈ Multiset(Multiset α), the product over the joined multiset equals the product of the inner products: prod (join S) = prod (map prod S).
Русский
Пусть α — коммутативный моноид. Для любого S ∈ Multiset(Multiset α) выполняется произведение по объединению: prod (join S) = prod (map prod S).
LaTeX
$$$\\mathrm{prod}(\\mathrm{join} S) = \\mathrm{prod}(\\mathrm{map} \\mathrm{prod} S)$$$
Lean4
@[to_additive (attr := simp)]
theorem prod_join [CommMonoid α] {S : Multiset (Multiset α)} : prod (join S) = prod (map prod S) := by
induction S using Multiset.induction with
| empty => simp
| cons _ _ ih => simp [ih]
