mathlib documentation


Field Structure on the Rational Numbers #

Summary #

We put the (discrete) field structure on the type of rational numbers that was defined in data.rat.defs.

Main Definitions #

Implementation notes #

We have to define the field structure in a separate file to avoid cyclic imports: the field class contains a map from (see field's docstring for the rationale), so we have a dependency rat.fieldfieldrat that is reflected in the import hierarchy data.rat.basic → algebra.field.basic → data.rat.defs.

Tags #

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