Theorem OrderDual.toDual_ofDual

Modification history

2025-12-26 13:27
Mathlib/Order/Synonym.lean
chore(Order/Synonym): use `to_dual` (#33266)
Modified OrderDual.toDual_ofDualView on Github →
2022-11-18 03:49
Mathlib/Order/Synonym.lean
feat: port Order.Synonym (#562) …
Added OrderDual.toDual_ofDualView on Github →