Commit 2023-01-18 10:57 b862c9b4

View on Github →

feat: port Data.Multiset.Sort (#1639)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/Sort.lean

added theorem Multiset.coe_sort

added theorem Multiset.length_sort

added theorem Multiset.mem_sort

added def Multiset.sort

added theorem Multiset.sort_eq

added theorem Multiset.sort_singleton

added theorem Multiset.sort_sorted

added theorem Multiset.sort_zero