Def LinearOrder.toDecidableLE'

Modification history

2026-02-03 15:41
Mathlib/Order/Defs/LinearOrder.lean
feat: unfold-boundaries in `to_dual` (#32438) …
Deleted LinearOrder.toDecidableLE'View on Github →
2025-11-19 22:18
Mathlib/Order/Defs/LinearOrder.lean
chore(Order/Defs/LinearOrder): use `@[to_dual]` (#31709) …
Added LinearOrder.toDecidableLE'View on Github →