The nonnegative rational numbers form a linear ordered commutative semiring

This file proves that the linear order on ℚ≥0 makes it into an ordered semiring.

ℚ≥0 is in fact a linearly ordered semifield. To access this fact, one must also import Mathlib/Algebra/Field/Rat.lean.

Tags

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

instance NNRat.instIsStrictOrderedRing : IsStrictOrderedRing ℚ≥0

instance NNRat.instCanonicallyOrderedAdd : CanonicallyOrderedAdd ℚ≥0

instance NNRat.instOrderedSub : OrderedSub ℚ≥0