The rational numbers form a linear ordered field

This file contains the linear ordered field instance on the rational numbers.

See note [foundational algebra order theory].

Tags

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

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 ⋯

Miscellaneous lemmas

@[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)

theorem NNRat.num_inv_of_ne_zero {q : ℚ≥0} (hq : q ≠ 0) : q⁻¹.num = q.den

theorem NNRat.den_inv_of_ne_zero {q : ℚ≥0} (hq : q ≠ 0) : q⁻¹.den = q.num