Theorem Ordering.compares_eq

Modification history

2024-09-13 20:11

Mathlib/Data/Ordering/Basic.lean

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

Modified Ordering.compares_eq View on Github →

2022-11-23 19:36

Mathlib/Order/Compare.lean

feat: port Logic.Equiv.Basic (#631) …

Added Ordering.compares_eq View on Github →