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.