Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-15 11:40 33daf353

View on Github →

feat(data/finset/basic): finset α is well-founded (#17950) and multiset α too.

Estimated changes

modified theorem multiset.to_finset_subset