mathlib3
8e09111f - chore(order/basic): add `strict_mono_??cr_on.dual` and `dual_right` (#5107)

Commit

5 years ago

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 β)`.

Author

urkud

Parents

a106102a

mathlib3 8e09111f - chore(order/basic): add `strict_mono_??cr_on.dual` and `dual_right` (#5107)

mathlib3
8e09111f - chore(order/basic): add `strict_mono_??cr_on.dual` and `dual_right` (#5107)