feat(data/multiset): the product of inverses is the inverse of the product (#7637)
feat(data/multiset): the product of inverses is the inverse of the product (#7637)

Entirely analogous to `prod_map_mul` defined above.





leanprover-community/mathlib,leanprover-community/mathlib