mathlib

7121691d - feat(data/multiset/basic): multiset inclusion is decidable (#16994)