Theorem ltByCases_ne

Modification history

2025-10-31 08:47

Mathlib/Order/Basic.lean

chore: remove declarations deprecated before 2025-04-21 (#30759) …

Deleted ltByCases_ne View on Github →

2024-01-12 12:47

Mathlib/Order/Basic.lean

feat(Order/Basic): Add `ltByCases` API (#9114) …

Added ltByCases_ne View on Github →