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

• Rat.instLinearOrderedField = LinearOrderedField.mk ⋯ Field.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Field.nnqsmul ⋯ ⋯ Field.qsmul ⋯