mathlib
c65146d6 - chore(data/finset/basic): erase_inj_on (#6769)

Commit

4 years ago

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

Author

pechersky

pechersky

Parents

Loading