mathlib
bada932c
- feat(data/multiset/basic): `erase_singleton` (#14094)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(data/multiset/basic): `erase_singleton` (#14094) Add `multiset.erase_singleton` which is analogous to the existing [finset.erase_singleton](https://leanprover-community.github.io/mathlib_docs/data/finset/basic.html#finset.erase_singleton).
Author
alreadydone
Parents
55671bee
Loading