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

Tags #

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

source

instance Rat.field :

Field ℚ

Equations

Rat.field = Field.mk zpowRec (_ : ∀ (a : ℚ), a ≠ 0 → a * a⁻¹ = 1) (_ : 0⁻¹ = 0) fun x x_1 => x * x_1

source

instance Rat.divisionRing :

DivisionRing ℚ

Equations

Rat.divisionRing = inferInstance