Sums over multiset cartesian products

[UPSTREAM] candidate: the Multiset analogue of Finset.sum_mul_sum, absent from mathlib.

theorem Multiset.sum_map_product_mul {α : Type u_1} {β : Type u_2} {M : Type u_3} [NonUnitalNonAssocSemiring M] (s : Multiset α) (t : Multiset β) (f : α → M) (g : β → M) : (map (fun (p : α × β) => f p.1 * g p.2) (s ×ˢ t)).sum = (map f s).sum * (map g t).sum

Sum of a pointwise product over a cartesian product factors as a product of sums.