mathlib

d3e20b4a - chore(data/multiset/basic): consistently use singleton notation (#8786)