Theorem ltTrichotomy_congr

Modification history

2025-10-31 08:47

Mathlib/Order/Basic.lean

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

Deleted ltTrichotomy_congr View on Github →

2024-01-12 12:47

Mathlib/Order/Basic.lean

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

Added ltTrichotomy_congr View on Github →