Theorem Ordering.swap_orElse

Modification history

2024-09-13 20:11

Mathlib/Order/Compare.lean

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

Modified Ordering.swap_orElse View on Github →

2022-11-18 04:44

Mathlib/Order/Compare.lean

feat: port Order.Compare (#569) …

Added Ordering.swap_orElse View on Github →