mathlib documentation

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.

Notations

Tags

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

def rat.nonneg  :
→ Prop

Equations
@[simp]
theorem rat.mk_nonneg (a : ) {b : } :
0 < b((a /. b).nonneg 0 a)

theorem rat.nonneg_add {a b : } :
a.nonnegb.nonneg(a + b).nonneg

theorem rat.nonneg_mul {a b : } :
a.nonnegb.nonneg(a * b).nonneg

theorem rat.nonneg_antisymm {a : } :
a.nonneg(-a).nonnega = 0

theorem rat.nonneg_total (a : ) :

@[instance]

Equations
def rat.le  :
→ Prop

Equations
@[instance]

Equations
@[instance]

Equations
theorem rat.le_def {a b c d : } :
0 < b0 < d(a /. b c /. 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 : } :
a bb aa = b

theorem rat.le_trans {a b c : } :
a bb ca c

@[instance]

Equations
@[instance]

Equations
theorem rat.le_def' {p q : } :
p q (p.num) * (q.denom) (q.num) * (p.denom)

theorem rat.lt_def {p q : } :
p < q (p.num) * (q.denom) < (q.num) * (p.denom)

theorem rat.nonneg_iff_zero_le {a : } :
a.nonneg 0 a

theorem rat.num_nonneg_iff_zero_le {a : } :
0 a.num 0 a

theorem rat.add_le_add_left {a b c : } :
c + a c + b a b

theorem rat.mul_nonneg {a b : } :
0 a0 b0 a * b

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 : } :
0 < b0 < d(a / b < c / d a * d < c * b)

theorem rat.lt_one_iff_num_lt_denom {q : } :
q < 1 q.num < (q.denom)

theorem rat.abs_def (q : ) :