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 ⋯

instance instNNRatCanonicallyLinearOrderedSemifield : CanonicallyLinearOrderedSemifield ℚ≥0

Equations

• instNNRatCanonicallyLinearOrderedSemifield = Nonneg.canonicallyLinearOrderedSemifield

instance instNNRatLinearOrderedSemifield : LinearOrderedSemifield ℚ≥0

Equations

• instNNRatLinearOrderedSemifield = Nonneg.linearOrderedSemifield

instance instNNRatLinearOrderedCommGroupWithZero : LinearOrderedCommGroupWithZero ℚ≥0

Equations

• instNNRatLinearOrderedCommGroupWithZero = Nonneg.linearOrderedCommGroupWithZero