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

instance Rat.field : Field ℚ

Equations

• Rat.field = Field.mk Rat.field.proof_1 zpowRec Rat.field.proof_2 Rat.field.proof_3 Rat.field.proof_4 ⋯ ⋯ Rat.field.proof_5 (fun (x x_1 : ℚ) => x * x_1) Rat.field.proof_6

instance Rat.divisionRing : DivisionRing ℚ

Equations

• Rat.divisionRing = inferInstance

instance Rat.instLinearOrderedField : LinearOrderedField ℚ

Equations

• Rat.instLinearOrderedField = let __src := Rat.field; let __src_1 := Rat.instLinearOrderedCommRing; LinearOrderedField.mk ⋯ Field.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Field.qsmul ⋯