The rational numbers form a linear ordered field

This file used to contain the linear ordered field instance on the rational numbers.

TODO: rename this file to Mathlib/Algebra/Order/GroupWithZero/NNRat.lean

See note [foundational algebra order theory].

Tags

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

@[implicit_reducible]

instance instLinearOrderedCommGroupWithZeroNNRat : LinearOrderedCommGroupWithZero ℚ≥0

Equations

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