mathlib3

8d426f04 - split(algebra/big_operators/multiset): Split off `data.multiset.basic` (#11043)

split(algebra/big_operators/multiset): Split off `data.multiset.basic` (#11043) This moves * `multiset.prod`, `multiset.sum` to `algebra.big_operators.multiset` * `multiset.join`, `multiset.bind`, `multiset.product`, `multiset.sigma` to `data.multiset.bind`. This is needed as `join` is defined using `sum`. The file was quite messy, so I reorganized `algebra.big_operators.multiset` by increasing typeclass assumptions. I'm crediting Mario for 0663945f55335e51c2b9b3a0177a84262dd87eaf (`prod`, `sum`, `join`), f9de18397dc1a43817803c2fe5d84b282287ed0d (`bind`, `product`), 16d40d7491d1fe8a733d21e90e516e0dd3f41c5b (`sigma`).