Theorem OrderDual.toDual_eq_top

Modification history

2025-12-05 13:19
Mathlib/Order/BoundedOrder/Basic.lean
chore(Order/BoundedOrder/Basic): use `to_dual` (#32377) …
Modified OrderDual.toDual_eq_topView on Github →
2025-11-18 16:33
Mathlib/Order/BoundedOrder/Basic.lean
feat: characterise regular elements of type synonyms (#31739)
Added OrderDual.toDual_eq_topView on Github →