The rational numbers form a linear ordered commutative ring #
This file proves that the linear order on ℚ makes it into an ordered ring.
ℚ is in fact a linearly ordered field. To access this fact, one must also import
Mathlib/Algebra/Field/Rat.lean.
Tags #
rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering