Theorem cmp_eq_compareOfLessAndEq

Modification history

2024-11-26 10:41
Mathlib/Order/Defs.lean
chore: split Order.Defs (#19498)
Modified cmp_eq_compareOfLessAndEqView on Github →
2024-10-08 06:33
Mathlib/Order/Defs.lean
feat: `LawfulOrd` and `LinearOrder` (#12082) …
Added cmp_eq_compareOfLessAndEqView on Github →