Commit 2025-05-25 21:04 8dbdfb1d
View on Github →feat: Finset.sort commutes with Finset.map (#25155)
We already had this lemma for Multiset.
For Finset, we can specialize to StrictMonoOn.
feat: Finset.sort commutes with Finset.map (#25155)
We already had this lemma for Multiset.
For Finset, we can specialize to StrictMonoOn.