BigOperators theorems for Multiset

Stream: mathlib4

[Martin Dvořák]

Do we want to systematically create Multiset versions of theorems from this file?
https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/List/BigOperators/Basic.lean
Otherwise, I'll PR only the one I need for my VCSP.

[Eric Wieser]

I would expect we already have many of them

[Eric Wieser]

There are a lot of weird theorems in that file due to multiplication not being commutative, which isn't allowed for docs#Multiset.prod

[Eric Wieser]

(it is for docs#Multiset.nonCommProd though...)

[Martin Dvořák]

Eric Wieser said:

I would expect we already have many of them

Which file(s) do you recommend checking?

[Eric Wieser]

Loogle?

[Martin Dvořák]

Back to my original question: Do we want to systematically add all those that can be proved for Multiset but are not in mathlib yet? Or should I just add the one I need now?

[Eric Wieser]

Adding just the one you need now (and the obvious variants of it) is fine, and shouldn't be held up by doing the whole file

[Eric Wieser]

But it might also be a good idea to do the whole file after you're unblocked

[Martin Dvořák]

#8127

[Martin Dvořák]

I think that, before we add the Multiset versions, we should address the inconsistencies between the List versions and the Finset versions. See my comment here:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Multiset.2Esum_lt_sum/near/400185099