mathlib

da24addb - feat(data/multiset): ordered sum lemmas (#4305)

feat(data/multiset): ordered sum lemmas (#4305) Add some lemmas about products in ordered monoids and sums in ordered add monoids, and a multiset count filter lemma (and a rename of a count filter lemma)