Documentation

Mathlib.Algebra.Field.Rat

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.