diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index 93e98d17b..d375c2c20 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -306,8 +306,9 @@ section migrate_algebra zero_lt_one := zero_lt_one, add_lt_add_left := @add_lt_add_left⦄ + local attribute rat.discrete_linear_ordered_field [trans-instance] local attribute rat.discrete_field [instance] - local attribute rat.discrete_linear_ordered_field [instance] + definition min : ℚ → ℚ → ℚ := algebra.min definition max : ℚ → ℚ → ℚ := algebra.max definition abs : ℚ → ℚ := algebra.abs