# Order for Rational Numbers #

This file constructs the order on ℚ and proves that ℚ is a discrete, linearly ordered commutative ring.

ℚ is in fact a linearly ordered field, but this fact is located in Data.Rat.Field instead of here because we need the order on ℚ to define ℚ≥0, which we itself need to define Field.

## Tags #

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

@[simp]
theorem Rat.num_nonneg {a : } :
0 a.num 0 a
@[simp]
theorem Rat.divInt_nonneg_iff_of_pos_right {a : } {b : } (hb : 0 < b) :
0 0 a
@[simp]
theorem Rat.divInt_nonneg {a : } {b : } (ha : 0 a) (hb : 0 b) :
0
@[simp]
theorem Rat.mkRat_nonneg {a : } (ha : 0 a) (b : ) :
0 mkRat a b
theorem Rat.ofScientific_nonneg (m : ) (s : Bool) (e : ) :
0
instance NNRatCast.toOfScientific {K : Type u_1} [] :
Equations
• NNRatCast.toOfScientific = { ofScientific := fun (m : ) (b : Bool) (d : ) => ⟨, }
@[simp]
theorem NNRat.cast_ofScientific {K : Type u_1} [] (m : ) (s : Bool) (e : ) :
() =

Casting a scientific literal via ℚ≥0 is the same as casting directly.

theorem Rat.add_nonneg {a : } {b : } :
0 a0 b0 a + b
theorem Rat.mul_nonneg {a : } {b : } :
0 a0 b0 a * b
theorem Rat.nonneg_antisymm {a : } :
0 a0 -aa = 0
theorem Rat.nonneg_total (a : ) :
0 a 0 -a
theorem Rat.le_iff_sub_nonneg (a : ) (b : ) :
a b 0 b - a
theorem Rat.divInt_le_divInt {a : } {b : } {c : } {d : } (b0 : 0 < b) (d0 : 0 < d) :
a * d c * b
theorem Rat.le_total {a : } {b : } :
a b b a
theorem Rat.not_le {a : } {b : } :
¬a b b < a
Equations
Equations
instance Rat.instLattice :
Equations
Equations
Equations
instance Rat.instInf :
Equations
instance Rat.instSup :
Equations
Equations
instance Rat.instPreorder :
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
Equations
Equations
Equations
Equations
Equations
Equations
@[simp]
theorem Rat.num_nonpos {a : } :
a.num 0 a 0
@[simp]
theorem Rat.num_pos {a : } :
0 < a.num 0 < a
@[simp]
theorem Rat.num_neg {a : } :
a.num < 0 a < 0
@[deprecated Rat.num_nonneg]
theorem Rat.num_nonneg_iff_zero_le {a : } :
0 a.num 0 a

Alias of Rat.num_nonneg.

@[deprecated Rat.num_pos]
theorem Rat.num_pos_iff_pos {a : } :
0 < a.num 0 < a

Alias of Rat.num_pos.

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 : ) :
|q| = Rat.divInt q.num.natAbs q.den