multiset.sum

Stream: general

[Antoine Labelle]

According to Main declarations in https://leanprover-community.github.io/mathlib_docs/algebra/big_operators/multiset.html, we have

multiset.sum: s.sum f is the sum of f i over all i ∈ s.

However, looking at the definition of multiset.sum, it doesn't seem to take a function f as an argument, instead it just gives the sum of the elements of the given multiset. Is that an error in the documentation?

[Yaël Dillies]

Yes, the docstring is wrong.

[Yaël Dillies]

It matters for finset to have an indexed sum because finsets don't have duplicates, but for multiset you can just map, then sum, so no need to index.