Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-17 18:10 4ab0e350

View on Github →

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

Estimated changes