Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-07 15:50 0e494afe

View on Github →

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.

Estimated changes