The rational numbers form a linear ordered field

This file contains the linear ordered field instance on the rational numbers.

See note [foundational algebra order theory].

Tags

rat, rationals, field, ℚ, numerator, denominator, num, denom

instance Rat.instLinearOrderedField : LinearOrderedField ℚ

Equations

• One or more equations did not get rendered due to their size.

instance instNNRatLinearOrderedSemifield : LinearOrderedSemifield ℚ≥0

Equations

• instNNRatLinearOrderedSemifield = Nonneg.linearOrderedSemifield

instance instNNRatLinearOrderedCommGroupWithZero : LinearOrderedCommGroupWithZero ℚ≥0

Equations

• instNNRatLinearOrderedCommGroupWithZero = Nonneg.linearOrderedCommGroupWithZero