Theorem cmpUsing_eq_lt

Modification history

2023-11-14 09:14

Mathlib/Init/Data/Ordering/Lemmas.lean

chore: bump Std (#8403)

Modified cmpUsing_eq_lt View on Github →

2023-05-24 01:45

Mathlib/Init/Data/Ordering/Lemmas.lean

feat: port Init.Data.Ordering.Lemmas (#4281)

Added cmpUsing_eq_lt View on Github →