mathlib3

c2d8bc2d - feat(data/finsupp): relatie to_multiset to 0, +, single, card, map, prod, and to_finset