multiset.sum

Stream: Is there code for X?

[Marcus Rossel]

Clicking on the "source" for multiset.sum shows the definition of multiset.prod. What is the definition of multiset.sum?

[Ruben Van de Velde]

It's translated automatically from prod by the to_additive attribute

[Eric Wieser]

#print multiset.sum will show you the translation

[Kevin Buzzard]

The answer is "it's the same but change all prods to sums, all monoids to add_monoids, all ->* to ->+ etc". More formally you can look at the definition of to_additive to see what the translation is