mathlib3
2cdded92 - feat(data/multiset/basic): add multiset.filter_singleton (#14938)

Commit
3 years ago
feat(data/multiset/basic): add multiset.filter_singleton (#14938) Adds a lemma, similar to `finset.filter_singleton`.
Author
Parents
Loading