English
For f : α →₀ ℕ and a commutative monoid, the product over the multiset represented by f equals the product over the underlying elements with their multiplicities: f.toMultiset.prod = ∏ a n => a^n, where n = f a.
Русский
Для f : α →₀ ℕ в коммутативном моноиде произведение мультимножества, соответствующего f, равно произведению элементов с учётом их кратностей: f.toMultiset.prod = ∏ a a^{f(a)}.
LaTeX
$$$f.\mathrm{toMultiset}.prod = f.prod\; (\lambda a\ n. a^n)$$$
Lean4
@[to_additive (attr := simp)]
theorem prod_toMultiset [CommMonoid α] (f : α →₀ ℕ) : f.toMultiset.prod = f.prod fun a n => a ^ n :=
by
refine f.induction ?_ ?_
· rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]
· intro a n f _ _ ih
rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]
exact pow_zero a
