Theorem OrderDual.Ord.dual_dual

Modification history

2026-02-11 10:09
Mathlib/Order/Basic.lean
chore: move OrderDual to its own file (#35105) …
Modified OrderDual.Ord.dual_dualView on Github →
2024-12-07 13:24
Mathlib/Order/Basic.lean
refactor(Order/Basic): Make `LinearOrder α = LinearOrder αᵒᵈᵒᵈ` defeq (#19776)
Added OrderDual.Ord.dual_dualView on Github →