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.instField 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.instField : Field ℚ

Equations

• One or more equations did not get rendered due to their size.

instance Rat.instDivisionRing : DivisionRing ℚ

Equations

• Rat.instDivisionRing = inferInstance

instance Rat.instLinearOrderedField : LinearOrderedField ℚ

Equations

• Rat.instLinearOrderedField = let __spread.0 := Rat.instLinearOrderedCommRing; let __spread.1 := Rat.instField; LinearOrderedField.mk ⋯ Field.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Field.nnqsmul ⋯ ⋯ Field.qsmul ⋯

@[simp]

theorem NNRat.coe_inv (q : ℚ≥0) : ↑q⁻¹ = (↑q)⁻¹

@[simp]

theorem NNRat.coe_div (p : ℚ≥0) (q : ℚ≥0) : ↑(p / q) = ↑p / ↑q

theorem NNRat.inv_def (q : ℚ≥0) : q⁻¹ = NNRat.divNat q.den q.num

theorem NNRat.div_def (p : ℚ≥0) (q : ℚ≥0) : p / q = NNRat.divNat (p.num * q.den) (p.den * q.num)