Mathlib Changelog
v4
Changelog
About
Github
Theorem
OrderIso.sorted_lt_listMap
Modification history
2025-12-05 15:16
Mathlib/Data/List/Sort.lean
refactor(`Data/List/Sort`): deprecate and replace `List.Sorted` (#30441) …
Deleted
OrderIso.sorted_lt_listMap
View on Github →
2025-03-03 08:08
Mathlib/Data/List/Sort.lean
feat(List/Sort): add lemmas about `(l.map f).Sorted _` (#22426)
Added
OrderIso.sorted_lt_listMap
View on Github →