mathlib
59facea4 - chore(data/multiset/basic): `∅` → `0` (#14211)

Commit
3 years ago
chore(data/multiset/basic): `∅` → `0` (#14211) It's preferred to use `0` instead of `∅` throughout the multiset API.
Author
Parents
Loading