Theorem compare_lt_iff_lt

Modification history

2024-11-26 10:41

Mathlib/Order/Defs.lean

chore: split Order.Defs (#19498)

Modified compare_lt_iff_lt View on Github →

2024-08-22 12:56

Mathlib/Order/Defs.lean

chore(Order/Defs): Cleanup (#16059)

Modified compare_lt_iff_lt View on Github →

2023-03-27 22:17

Mathlib/Init/Algebra/Order.lean

feat: `LinearOrder α` extends `Ord α` (#2858) …

Added compare_lt_iff_lt View on Github →