Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-12 23:17 a6d445db

View on Github →

feat(data/finsupp): Add map_finsupp_prod to homs (#4585) This is a convenience alias for map_prod, which is awkward to use.

Estimated changes