Def Ordering.Compares

Modification history

2024-09-13 20:11

Mathlib/Data/Ordering/Basic.lean

chore: deprecate `Ordering.orElse` for `.then` (#12068) …

Modified Ordering.Compares View on Github →

2022-11-18 04:44

Mathlib/Order/Compare.lean

feat: port Order.Compare (#569) …

Added Ordering.Compares View on Github →