mathlib3
2a286527 - feat(data/finset/basic): add filter_erase (#10384)

Commit
4 years ago
feat(data/finset/basic): add filter_erase (#10384) Like `filter_insert`, but for `erase`
Author
Parents
Loading