# Documentation

Mathlib.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 Mathlib.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→ Field → Rat→ Rat that is reflected in the import hierarchy Mathlib.Data.Rat.basic → Mathlib.Algebra.Field.Defs → Std.Data.Rat→ Mathlib.Algebra.Field.Defs → Std.Data.Rat→ Std.Data.Rat.

## Tags #

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

instance Rat.field :
Equations
instance Rat.divisionRing :
Equations