# Documentation

Mathlib.Data.Rat.Order

# Order for Rational Numbers #

## Summary #

We define the order on ℚ, prove that ℚ is a discrete, linearly ordered field, and define functions such as abs and sqrt that depend on this order.

## Tags #

rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering, sqrt, abs

def Rat.Nonneg (r : ) :

A rational number is called nonnegative if its numerator is nonnegative.

Equations
@[simp]
theorem Rat.divInt_nonneg (a : ) {b : } (h : 0 < b) :
theorem Rat.nonneg_add {a : } {b : } :
Rat.Nonneg (a + b)
theorem Rat.nonneg_mul {a : } {b : } :
Rat.Nonneg (a * b)
theorem Rat.nonneg_antisymm {a : } :
Rat.Nonneg (-a)a = 0
instance Rat.decidableNonneg (a : ) :
Equations
• = Rat.casesOn (motive := fun t => a = t) a (fun num den den_nz reduced h => (_ : Rat.mk' num den = a)id inferInstance) (_ : a = a)
def Rat.le' (a : ) (b : ) :

Relation a ≤ b on ℚ defined as a ≤ b ↔ Rat.Nonneg (b - a). Use a ≤ b instead of Rat.le a b.

Equations
def Rat.numDenCasesOn'' {C : Sort u} (a : ) (H : (n : ) → (d : ) → (nz : d 0) → (red : ) → C (Rat.mk' n d)) :
C a

Define a (dependent) function or prove ∀ r : ℚ, p r by dealing with rational numbers of the form mk' n d with d ≠ 0.

Equations
theorem Rat.le_iff_Nonneg (a : ) (b : ) :
a b Rat.Nonneg (b - a)
theorem Rat.le_def {a : } {b : } {c : } {d : } (b0 : 0 < b) (d0 : 0 < d) :
a * d c * b
theorem Rat.le_refl (a : ) :
a a
theorem Rat.le_total (a : ) (b : ) :
a b b a
theorem Rat.le_antisymm {a : } {b : } (hab : a b) (hba : b a) :
a = b
theorem Rat.le_trans {a : } {b : } {c : } (hab : a b) (hbc : b c) :
a c
theorem Rat.not_le {a : } {b : } :
¬a b b < a
instance Rat.linearOrder :
Equations
instance Rat.instLTRat_1 :
Equations
Equations
instance Rat.instInfRat :
Equations
instance Rat.instSupRat :
Equations
Equations
theorem Rat.le_def' {p : } {q : } :
p q p.num * q.den q.num * p.den
theorem Rat.lt_def {p : } {q : } :
p < q p.num * q.den < q.num * p.den
theorem Rat.add_le_add_left {a : } {b : } {c : } :
c + a c + b a b
theorem Rat.mul_nonneg {a : } {b : } (ha : 0 a) (hb : 0 b) :
0 a * b
Equations
• One or more equations did not get rendered due to their size.
Equations
theorem Rat.num_pos_iff_pos {a : } :
0 < a.num 0 < a
theorem Rat.div_lt_div_iff_mul_lt_mul {a : } {b : } {c : } {d : } (b_pos : 0 < b) (d_pos : 0 < d) :
a / b < c / d a * d < c * b
theorem Rat.lt_one_iff_num_lt_denom {q : } :
q < 1 q.num < q.den
theorem Rat.abs_def (q : ) :
abs q = Rat.divInt ↑(Int.natAbs q.num) q.den