Using zero for the empty (multi)set

Stream: new members

[Harry Richman]

I noticed in the documentation for Multiset that 0 is used to denote the empty multiset. I was wondering, what is the motivation for this choice, rather than ∅? Is it something as simple as being easier to type, or it's arbitrary, or is there a deeper reason? This caused me some confusion, since I would consider ∅ more "standard" notation in mathematical usage.

Is it also true that 0 is used for the empty set in other set-like types (e.g. Set, Finset, ...)? I tried to search the documentation but could not find the answer quickly.

---

In particular, I was confused the theorem Polynomial.roots_zero about the roots of a constant polynomial:

@[simp]
theorem roots_zero : (0 : R[X]).roots = 0 :=
  dif_pos rfl

I initially suspected a typo, where 0 should be ∅, but found out that in fact 0 is allowed (and defined!) to denote the empty multiset.

[Aaron Liu]

Multisets here are special because they form a docs#Multiset.instAddCancelCommMonoid

[Eric Wieser]

Though it's not clear why we decided that multisets should be the free commutative additive monoid, but lists shouldn't be the free noncommutative additive monoid (which is instead docs#FreeAddMonoid).