mathlib

b9c17c14 - feat(data/multiset/fintype): coercion from multiset to type (#15094)

feat(data/multiset/fintype): coercion from multiset to type (#15094) Introduces a coercion from multisets to types and provides a `fintype` instance for it. Also gives some definitions and lemmas to help work with sums and products over multisets.