Commit 2024-11-03 17:58 1e306b12

View on Github →

feat(Data/Finset/Sort): sort (range n) = range n (#18465)

Estimated changes

Modified Mathlib/Data/Finset/Sort.lean

added theorem Finset.sort_range

Modified Mathlib/Data/List/Sort.lean

added theorem List.sorted_le_range

added theorem List.sorted_lt_range

Modified Mathlib/Data/Multiset/Sort.lean

added theorem Multiset.sort_range