mathlib3
4ab0e350 - feat(data/multiset): the product of inverses is the inverse of the product (#7637)

Commit

4 years ago

feat(data/multiset): the product of inverses is the inverse of the product (#7637) Entirely analogous to `prod_map_mul` defined above.

Author

Vierkantor

Parents