Commit 2020-10-09 13:16 306dc8a0

chore(algebra/big_operators/basic): add lemma prod_multiset_count' that generalize prod_multiset_count to consider a function to a monoid (#4534) I have added prod_multiset_count' that is very similar to prod_multiset_count but takes into account a function f : \a \r M where M is a commutative monoid. The proof is essentially the same (I didn't try to prove it using prod_multiset_count because maybe we can remove it and just keep the more general version).