Commit 2021-12-25 19:14 8d426f04
View on Github →split(algebra/big_operators/multiset): Split off data.multiset.basic
(#11043)
This moves
multiset.prod
,multiset.sum
toalgebra.big_operators.multiset
multiset.join
,multiset.bind
,multiset.product
,multiset.sigma
todata.multiset.bind
. This is needed asjoin
is defined usingsum
. The file was quite messy, so I reorganizedalgebra.big_operators.multiset
by increasing typeclass assumptions. I'm crediting Mario for 0663945f55335e51c2b9b3a0177a84262dd87eaf (prod
,sum
,join
), f9de18397dc1a43817803c2fe5d84b282287ed0d (bind
,product
), 16d40d7491d1fe8a733d21e90e516e0dd3f41c5b (sigma
).