Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-19 19:07 c65146d6

View on Github →

chore(data/finset/basic): erase_inj_on (#6769) Quick follow-up to #6737

Estimated changes

added theorem finset.erase_inj_on