Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-22 10:49 43cd79f9

View on Github →

feat(data/finset/basic): Simple finset.erase lemmas (#9878) finset.erase.singleton and finset.(map/image)_erase

Estimated changes

added theorem finset.erase_singleton
added theorem finset.image_erase
added theorem finset.map_erase