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 #

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 Mathlib.Data.Rat.basic → Mathlib.Algebra.Field.DefsStd.Data.Rat.

Tags #

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