English
Let f : α →₀ M with M an additive commutative monoid and h : α → M → Multiset N for some additive structure N. Then summing the multisets in a finsupp sense and then taking the multiset sum is the same as summing the multisets obtained by first summing in M and then summing in N: Multiset.sum (f.sum h) = f.sum (λ a b, Multiset.sum (h a b)).
Русский
Пусть f : α →₀ M, h : α → M → Multiset N; тогда двойное суммирование мультисета эквивалентно поочередному суммированию: Multiset.sum (f.sum h) = f.sum (λ a b, Multiset.sum (h a b)).
LaTeX
$$$\operatorname{Multiset}.sum\big(f.sum h\big) = f.sum\big(\\lambda a b, \operatorname{Multiset}.sum\big(h a b\big)\\right)$.$$
Lean4
theorem multiset_sum_sum [Zero M] [AddCommMonoid N] {f : α →₀ M} {h : α → M → Multiset N} :
Multiset.sum (f.sum h) = f.sum fun a b => Multiset.sum (h a b) :=
map_sum Multiset.sumAddMonoidHom _ f.support
