mathlib3

702b1e8c - refactor(data/finsupp/basic): merge `finsupp.of_multiset` and `multiset.to_finsupp` (#5237)

refactor(data/finsupp/basic): merge `finsupp.of_multiset` and `multiset.to_finsupp` (#5237) * redefine `finsupp.to_multiset` as an `add_equiv`; * drop `finsupp.equiv_multiset` and `finsupp.of_multiset`; * define `multiset.to_finsupp` as `finsupp.to_multiset.symm`.