Commit 2022-11-20 15:51 6c17afb9

View on Github →

feat(data/finset/basic): Map finset.filter under an equiv (#17513) Rename finset.map_filter to finset.filter_map. This unfortunately means it doesn't match the multiset and list lemmas. Prove the true finset.map_filter.

Estimated changes