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

@[simp]

theorem Rat.mkRat_nonneg {a : ℤ} (ha : 0 ≤ a) (b : ℕ) : 0 ≤ mkRat a b

theorem Rat.ofScientific_nonneg (m : ℕ) (s : Bool) (e : ℕ) : 0 ≤ Rat.ofScientific m s e

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, ⋯⟩ }

@[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.

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

theorem Rat.lt_iff_le_not_ge (a b : ℚ) : a < b ↔ a ≤ b ∧ ¬b ≤ a

instance Rat.linearOrder : LinearOrder ℚ

Equations

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

theorem Rat.mkRat_nonneg_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) : 0 ≤ mkRat a b ↔ 0 ≤ a

theorem Rat.mkRat_pos_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) : 0 < mkRat a b ↔ 0 < a

theorem Rat.mkRat_pos {a : ℤ} (ha : 0 < a) {b : ℕ} (hb : b ≠ 0) : 0 < mkRat a b

theorem Rat.mkRat_nonpos_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) : mkRat a b ≤ 0 ↔ a ≤ 0

theorem Rat.mkRat_nonpos {a : ℤ} (ha : a ≤ 0) (b : ℕ) : mkRat a b ≤ 0

theorem Rat.mkRat_neg_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) : mkRat a b < 0 ↔ a < 0

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.

instance Rat.instDistribLattice : DistribLattice ℚ

Equations

• Rat.instDistribLattice = inferInstance

instance Rat.instLattice : Lattice ℚ

Equations

• Rat.instLattice = inferInstance

instance Rat.instSemilatticeInf : SemilatticeInf ℚ

Equations

• Rat.instSemilatticeInf = inferInstance

instance Rat.instSemilatticeSup : SemilatticeSup ℚ

Equations

• Rat.instSemilatticeSup = inferInstance

instance Rat.instInf : Min ℚ

Equations

• Rat.instInf = inferInstance

instance Rat.instSup : Max ℚ

Equations

• Rat.instSup = inferInstance

instance Rat.instPartialOrder : PartialOrder ℚ

Equations

• Rat.instPartialOrder = inferInstance

instance Rat.instPreorder : Preorder ℚ

Equations

• Rat.instPreorder = inferInstance

Miscellaneous lemmas

@[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.

@[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.

instance Rat.instAddLeftMono : AddLeftMono ℚ

@[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

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| = divInt ↑q.num.natAbs ↑q.den