The rational numbers form a linear ordered field #
This file constructs the order on ℚ and proves that ℚ is a discrete, linearly ordered
commutative ring.
ℚ is in fact a linearly ordered field, but this fact is located in Data.Rat.Field instead of
here because we need the order on ℚ to define ℚ≥0, which we itself need to define Field.
Tags #
rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering