data.rat.basic

# 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 #

• rat.field is the field structure on ℚ.

## 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.field → field → rat that is reflected in the import hierarchy data.rat.basic → algebra.field.basic → data.rat.defs.

## Tags #

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

@[protected, instance]
def rat.field  :
Equations
@[protected, instance]
Equations