Def LinearOrder.toDecidableLT'

Modification history

2025-11-19 22:18
Mathlib/Order/Defs/LinearOrder.lean
chore(Order/Defs/LinearOrder): use `@[to_dual]` (#31709) …
Added LinearOrder.toDecidableLT'View on Github →