Theorem LinearOrder.ext_lt

Modification history

2025-04-06 17:49

Mathlib/Order/Basic.lean

chore(Order/Basic): order lemmas according to `Preorder`/`PartialOrder`/`LinearOrder` (#23624) …

Modified LinearOrder.ext_lt View on Github →

2024-12-07 13:24

Mathlib/Order/Basic.lean

feat(Order/Basic): `PartialOrder.ext_lt` (#19724) …

Added LinearOrder.ext_lt View on Github →