mathlib
0e494afe - chore(order/*): Less `order_dual` abuse (#14008)

Commit
3 years ago
chore(order/*): Less `order_dual` abuse (#14008) Sanitize uses of `order_dual` by inserting the required `of_dual` and `to_dual` instead of type-ascripting. Also remove some uses which were not necessary. Those dated from the time where we did not have antitone functions.
Author
Parents
Loading