mathlib3

a057441e - feat(order/basic): Notation for `order_dual` (#13798)

feat(order/basic): Notation for `order_dual` (#13798) Define `αᵒᵈ` as notation for `order_dual α` and replace current uses. [Zulip poll](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20order_dual/near/280629129)