Commit 2026-10-16 19:45 2f3c7c8a

feat(Data/Fin/Tuple/Sort): add descending sort Tuple.sortDesc (#43741) Add Tuple.sortDesc, the permutation sorting a tuple f : Fin n → α into decreasing order, as the antitone counterpart of Tuple.sort. Along with it:

• Tuple.antitone_sortDesc: f ∘ Tuple.sortDesc f is Antitone (mirrors Tuple.monotone_sort);
• Tuple.comp_perm_comp_sortDesc_eq_comp_sortDesc: the descending sorts of f and of any permutation of f agree (mirrors comp_perm_comp_sort_eq_comp_sort). Split out of #41898 (majorization), which needs the decreasing rearrangement of a tuple; these are general-purpose additions to the tuple-sorting API and belong next to Tuple.sort.