Documentation

Mathlib.Algebra.Order.Field.Rat

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

Equations

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