Documentation

Mathlib.Algebra.Order.Ring.Rat

The rational numbers form a linear ordered field #

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

source
@[simp]
theorem Rat.divInt_nonneg_iff_of_pos_right {a : ℤ} {b : ℤ} (hb : 0 < b) :
0 ≤ Rat.divInt a b ↔ 0 ≤ a
source
@[simp]
theorem Rat.divInt_nonneg {a : ℤ} {b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ Rat.divInt a b
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
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.add_nonneg {a : ℚ} {b : ℚ} :
0 ≤ a → 0 ≤ b → 0 ≤ a + b
source
theorem Rat.mul_nonneg {a : ℚ} {b : ℚ} :
0 ≤ a → 0 ≤ b → 0 ≤ a * b
source
theorem Rat.le_iff_sub_nonneg (a : ℚ) (b : ℚ) :
a ≤ b ↔ 0 ≤ b - a
source
theorem Rat.divInt_le_divInt {a : ℤ} {b : ℤ} {c : ℤ} {d : ℤ} (b0 : 0 < b) (d0 : 0 < d) :
Rat.divInt a b ≤ Rat.divInt c d ↔ a * d ≤ c * b
source
theorem Rat.le_total {a : ℚ} {b : ℚ} :
a ≤ b ∨ b ≤ a
source
theorem Rat.not_le {a : ℚ} {b : ℚ} :
¬a ≤ b ↔ b < a
source
instance Rat.linearOrder :
LinearOrder ℚ
Equations

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
source
instance Rat.instLattice :
Lattice ℚ
Equations
source
instance Rat.instSemilatticeInf :
SemilatticeInf ℚ
Equations
source
instance Rat.instSemilatticeSup :
SemilatticeSup ℚ
Equations
source
instance Rat.instInf :
Inf ℚ
Equations
source
instance Rat.instSup :
Sup ℚ
Equations
source
instance Rat.instPartialOrder :
PartialOrder ℚ
Equations
source
instance Rat.instPreorder :
Preorder ℚ
Equations

Miscellaneous lemmas #

source
theorem Rat.le_def {p : ℚ} {q : ℚ} :
p ≤ q ↔ p.num * ↑q.den ≤ q.num * ↑p.den
source
theorem Rat.lt_def {p : ℚ} {q : ℚ} :
p < q ↔ p.num * ↑q.den < q.num * ↑p.den
source
theorem Rat.add_le_add_left {a : ℚ} {b : ℚ} {c : ℚ} :
c + a ≤ c + b ↔ a ≤ b
source
instance Rat.instLinearOrderedCommRing :
LinearOrderedCommRing ℚ
Equations
source
instance Rat.instLinearOrderedRing :
LinearOrderedRing ℚ
Equations
source
instance Rat.instOrderedRing :
OrderedRing ℚ
Equations
source
instance Rat.instLinearOrderedSemiring :
LinearOrderedSemiring ℚ
Equations
source
instance Rat.instOrderedSemiring :
OrderedSemiring ℚ
Equations
source
instance Rat.instLinearOrderedAddCommGroup :
LinearOrderedAddCommGroup ℚ
Equations
source
instance Rat.instOrderedAddCommGroup :
OrderedAddCommGroup ℚ
Equations
source
instance Rat.instOrderedCancelAddCommMonoid :
OrderedCancelAddCommMonoid ℚ
Equations
source
instance Rat.instOrderedAddCommMonoid :
OrderedAddCommMonoid ℚ
Equations
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
@[deprecated Rat.num_nonneg]
theorem Rat.num_nonneg_iff_zero_le {q : ℚ} :
0 ≤ q.num ↔ 0 ≤ q

Alias of Rat.num_nonneg.

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

Alias of Rat.num_pos.

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