# The rational numbers form a field #

This file contains the field instance on the rational numbers.

See note [foundational algebra order theory].

## TODO #

Move the `Semifield ℚ≥0`

instance here. This will involve proving it by hand rather than relying on
the `Nonneg`

machinery.

## Tags #

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

## Equations

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

### Extra instances to short-circuit type class resolution #

These also prevent non-computable instances being used to construct these instances non-computably.