# The rational numbers possess a linear order #

This file constructs the order on `ℚ` and proves various facts relating the order to ring structure on `ℚ`. This only uses unbundled type classes, e.g. `CovariantClass`, relating the order structure and algebra structure on `ℚ`. For the bundled `LinearOrderedCommRing` instance on `ℚ`, see `Algebra.Order.Ring.Rat`.

## Tags #

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

source
@[simp]
theorem Rat.mkRat_nonneg {a : ℤ} (ha : 0 ≤ a) (b : ℕ) :
0 ≤ mkRat a b
source
theorem Rat.ofScientific_nonneg (m : ℕ) (s : Bool) (e : ℕ) :
0 ≤ Rat.ofScientific m s e
source
instance NNRatCast.toOfScientific {K : Type u_1} [NNRatCast K] :
OfScientific K
Equations

- NNRatCast.toOfScientific = { ofScientific := fun (m : ℕ) (b : Bool) (d : ℕ) => ↑⟨Rat.ofScientific m b d, ⋯⟩ }

source
theorem NNRatCast.toOfScientific_def {K : Type u_1} [NNRatCast K] (m : ℕ) (b : Bool) (d : ℕ) :
OfScientific.ofScientific m b d = ↑⟨OfScientific.ofScientific m b d, ⋯⟩
source
@[simp]
theorem NNRat.cast_ofScientific {K : Type u_1} [NNRatCast K] (m : ℕ) (s : Bool) (e : ℕ) :
↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e

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

source
theorem Rat.divInt_le_divInt {a b c d : ℤ} (b0 : 0 < b) (d0 : 0 < d) :
divInt a b ≤ divInt c d ↔ a * d ≤ c * b
source
theorem Rat.lt_iff_le_not_ge (a b : ℚ) :
a < b ↔ a ≤ b ∧ ¬b ≤ a
source
instance Rat.linearOrder :
LinearOrder ℚ
Equations

- One or more equations did not get rendered due to their size.

source
theorem Rat.mkRat_nonneg_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) :
0 ≤ mkRat a b ↔ 0 ≤ a
source
theorem Rat.mkRat_pos_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) :
0 < mkRat a b ↔ 0 < a
source
theorem Rat.mkRat_pos {a : ℤ} (ha : 0 < a) {b : ℕ} (hb : b ≠ 0) :
0 < mkRat a b
source
theorem Rat.mkRat_nonpos_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) :
mkRat a b ≤ 0 ↔ a ≤ 0
source
theorem Rat.mkRat_nonpos {a : ℤ} (ha : a ≤ 0) (b : ℕ) :
mkRat a b ≤ 0
source
theorem Rat.mkRat_neg_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) :
mkRat a b < 0 ↔ a < 0
source
theorem Rat.mkRat_neg {a : ℤ} (ha : a < 0) {b : ℕ} (hb : b ≠ 0) :
mkRat a b < 0

### Extra instances to short-circuit type class resolution #

These also prevent non-computable instances being used to construct these instances non-computably.

source
instance Rat.instDistribLattice :
DistribLattice ℚ
Equations

- Rat.instDistribLattice = inferInstance

source
instance Rat.instLattice :
Lattice ℚ
Equations

- Rat.instLattice = inferInstance

source
instance Rat.instSemilatticeInf :
SemilatticeInf ℚ
Equations

- Rat.instSemilatticeInf = inferInstance

source
instance Rat.instSemilatticeSup :
SemilatticeSup ℚ
Equations

- Rat.instSemilatticeSup = inferInstance

source
instance Rat.instInf :
Min ℚ
Equations

- Rat.instInf = inferInstance

source
instance Rat.instSup :
Max ℚ
Equations

- Rat.instSup = inferInstance

source
instance Rat.instPartialOrder :
PartialOrder ℚ
Equations

- Rat.instPartialOrder = inferInstance

source
instance Rat.instPreorder :
Preorder ℚ
Equations

- Rat.instPreorder = inferInstance

### Miscellaneous lemmas #

source
@[deprecated Rat.le_iff (since := "2025-08-14")]
theorem Rat.le_def (a b : ℚ) :
a ≤ b ↔ a.num * ↑b.den ≤ b.num * ↑a.den

Alias of `Rat.le_iff`.

source
@[deprecated Rat.lt_iff (since := "2025-08-14")]
theorem Rat.lt_def (a b : ℚ) :
a < b ↔ a.num * ↑b.den < b.num * ↑a.den

Alias of `Rat.lt_iff`.

source
instance Rat.instAddLeftMono :
AddLeftMono ℚ
source
@[simp]
theorem Rat.num_nonpos {a : ℚ} :
a.num ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem Rat.num_pos {a : ℚ} :
0 < a.num ↔ 0 < a
source
@[simp]
theorem Rat.num_neg {a : ℚ} :
a.num < 0 ↔ a < 0
source
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
source
theorem Rat.lt_one_iff_num_lt_denom {q : ℚ} :
q < 1 ↔ q.num < ↑q.den
source
theorem Rat.abs_def (q : ℚ) :
|q| = divInt ↑q.num.natAbs ↑q.den
source
theorem Rat.abs_def' (q : ℚ) :
|q| = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }
source
@[simp]
theorem Rat.num_abs_eq_abs_num (q : ℚ) :
|q|.num = |q.num|
source
@[simp]
theorem Rat.den_abs_eq_den (q : ℚ) :
|q|.den = q.den