Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-15 13:22 3a6340cc

View on Github →

chore(data/dfinsupp): golf using quotient.map instead of quotient.lift_on (#9176)

Estimated changes

modified def dfinsupp.erase
modified def dfinsupp.filter
modified def dfinsupp.map_range
modified def dfinsupp.zip_with