Documentation

Mathlib.Algebra.Order.Ring.Unbundled.Rat

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, eg 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.divInt_nonneg_iff_of_pos_right {a b : ℤ} (hb : 0 < b) :

0 ≤ divInt a b ↔ 0 ≤ a

@[simp]

theorem Rat.divInt_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) :

0 ≤ divInt a b

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

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.add_nonneg {a b : ℚ} :

0 ≤ a → 0 ≤ b → 0 ≤ a + b

theorem Rat.mul_nonneg {a b : ℚ} :

0 ≤ a → 0 ≤ b → 0 ≤ a * b

theorem Rat.not_le {a b : ℚ} :

¬a ≤ b ↔ b < a

theorem Rat.not_lt {a b : ℚ} :

¬a < b ↔ b ≤ a

theorem Rat.lt_iff (a b : ℚ) :

a < b ↔ a.num * ↑b.den < b.num * ↑a.den

theorem Rat.le_iff (a b : ℚ) :

a ≤ b ↔ a.num * ↑b.den ≤ b.num * ↑a.den

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) :

divInt a b ≤ divInt c d ↔ a * d ≤ c * b

theorem Rat.le_total {a b : ℚ} :

a ≤ b ∨ b ≤ a

instance Rat.linearOrder :

LinearOrder ℚ

Equations

Rat.linearOrder = LinearOrder.mk ⋯ inferInstance inferInstance inferInstance Rat.linearOrder.proof_5 Rat.linearOrder.proof_6 Rat.linearOrder.proof_7

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 :

Equations

Rat.instLattice = inferInstance

instance Rat.instSemilatticeInf :

SemilatticeInf ℚ

Equations

Rat.instSemilatticeInf = inferInstance

instance Rat.instSemilatticeSup :

SemilatticeSup ℚ

Equations

Rat.instSemilatticeSup = inferInstance

instance Rat.instInf :

Equations

Rat.instInf = inferInstance

instance Rat.instSup :

Equations

Rat.instSup = inferInstance

instance Rat.instPartialOrder :

PartialOrder ℚ

Equations

Rat.instPartialOrder = inferInstance

instance Rat.instPreorder :

Equations

Rat.instPreorder = inferInstance

Miscellaneous lemmas #

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

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