mathlib
899bb5f9
- feat(data/multiset): `(s.erase x).map f = (s.map f).erase (f x)` (#8375)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
feat(data/multiset): `(s.erase x).map f = (s.map f).erase (f x)` (#8375) A little lemma that I needed for Dedekind domains. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Author
Vierkantor
Parents
4676b31f
Loading