Commit 2025-10-22 00:08 1bbe77d5

View on Github →

feat(Data/{Finset,Multiset}/Sort): give sort functions ≤ default argument (#27864) Changes the Finset.sort and Multiset.sort functions to take ≤ as the default relation argument. Then removes this argument where possible through the rest of the library. This involves switching the order of arguments, but I think this is fine, as this function is mostly called by dot notation anyway, and I think it is more typical for the first argument of such functions to have the type that matches the namespace. Thanks to @eric-wieser for suggesting this approach Zulip discussion: #mathlib4 > Redefine {Fin/Multi}set.sort to take linear order?

Estimated changes

modified theorem Finset.length_sort
modified theorem Finset.map_sort
modified theorem Finset.mem_sort
modified def Finset.sort
modified theorem Finset.sort_cons
modified theorem Finset.sort_empty
modified theorem Finset.sort_eq
modified theorem Finset.sort_insert
modified theorem Finset.sort_mk
modified theorem Finset.sort_nodup
modified theorem Finset.sort_perm_toList
modified theorem Finset.sort_range
modified theorem Finset.sort_singleton
modified theorem Finset.sort_sorted
modified theorem Finset.sort_sorted_gt
modified theorem Finset.sort_sorted_lt
modified theorem Finset.sort_toFinset
modified theorem Finset.sort_val
modified theorem Finset.sorted_zero_eq_min'
modified theorem Multiset.coe_sort
modified theorem Multiset.length_sort
modified theorem Multiset.map_sort
modified theorem Multiset.mem_sort
modified def Multiset.sort
modified theorem Multiset.sort_cons
modified theorem Multiset.sort_eq
modified theorem Multiset.sort_range
modified theorem Multiset.sort_singleton
modified theorem Multiset.sort_sorted
modified theorem Multiset.sort_zero