Documentation

Mathlib.Algebra.Order.Field.Rat

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