mathlib3

1e594c77 - chore(data/multiset/basic): move theorems around (#15882)

chore(data/multiset/basic): move theorems around (#15882) This PR does the following: - move the `singleton` instance earlier (I want this defined before `to_list` for a subsequent PR) - move the `order_bot` instance earlier and minor golfs