Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-27 09:16 8e09111f

View on Github →

chore(order/basic): add strict_mono_??cr_on.dual and dual_right (#5107) We can use these to avoid @strict_mono_??cr_on (order_dual α) (order_dual β).

Estimated changes