mathlib3
fix(order.basic|ring_theory.algebra): lower instance priority
#1729
Merged
Merged