Theorem List.erase_orderedInsert

Modification history

2026-01-09 08:53
Mathlib/Data/List/Sort.lean
chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl` (#33755)
Modified List.erase_orderedInsertView on Github →
2024-03-07 21:56
Mathlib/Data/List/Sort.lean
feat: results about `List.orderedInsert` (#11191) …
Added List.erase_orderedInsertView on Github →