Documentation

Mathlib.Data.Rat.Order

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

source
@[simp]
theorem Rat.num_nonneg {a : ℚ} :
0 ≤ a.num ↔ 0 ≤ a
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
  • NNRatCast.toOfScientific = { ofScientific := fun (m : ℕ) (b : Bool) (d : ℕ) => ↑{ val := Rat.ofScientific m b d, property := ⋯ } }
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.nonneg_antisymm {a : ℚ} :
0 ≤ a → 0 ≤ -a → a = 0
source
theorem Rat.nonneg_total (a : ℚ) :
0 ≤ a ∨ 0 ≤ -a
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
  • One or more equations did not get rendered due to their size.
source
instance Rat.instLTRat_1 :
LT ℚ
Equations
source
instance Rat.instDistribLatticeRat :
DistribLattice ℚ
Equations
source
instance Rat.instLatticeRat :
Lattice ℚ
Equations
source
instance Rat.instSemilatticeInfRat :
SemilatticeInf ℚ
Equations
source
instance Rat.instSemilatticeSupRat :
SemilatticeSup ℚ
Equations
source
instance Rat.instInfRat :
Inf ℚ
Equations
source
instance Rat.instSupRat :
Sup ℚ
Equations
source
instance Rat.instPartialOrderRat :
PartialOrder ℚ
Equations
source
instance Rat.instPreorderRat :
Preorder ℚ
Equations
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.instLinearOrderedRingRat :
LinearOrderedRing ℚ
Equations
source
instance Rat.instOrderedRingRat :
OrderedRing ℚ
Equations
source
instance Rat.instLinearOrderedSemiringRat :
LinearOrderedSemiring ℚ
Equations
source
instance Rat.instOrderedSemiringRat :
OrderedSemiring ℚ
Equations
source
instance Rat.instLinearOrderedAddCommGroupRat :
LinearOrderedAddCommGroup ℚ
Equations
source
instance Rat.instOrderedAddCommGroupRat :
OrderedAddCommGroup ℚ
Equations
source
instance Rat.instOrderedCancelAddCommMonoidRat :
OrderedCancelAddCommMonoid ℚ
Equations
source
instance Rat.instOrderedAddCommMonoidRat :
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 {a : ℚ} :
0 ≤ a.num ↔ 0 ≤ a

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 ↑(Int.natAbs q.num) ↑q.den