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

source
@[simp]
theorem Rat.divInt_nonneg_iff_of_pos_right {a b : ℤ} (hb : 0 < b) :
0 ≤ divInt a b ↔ 0 ≤ a
source
@[simp]
theorem Rat.divInt_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ 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.not_le {a b : ℚ} :
    ¬a ≤ b ↔ b < a
    source
    theorem Rat.not_lt {a b : ℚ} :
    ¬a < b ↔ b ≤ a
    source
    theorem Rat.lt_iff (a b : ℚ) :
    a < b ↔ a.num * ↑b.den < b.num * ↑a.den
    source
    theorem Rat.le_iff (a b : ℚ) :
    a ≤ b ↔ a.num * ↑b.den ≤ b.num * ↑a.den
    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) :
    divInt a b ≤ divInt c d ↔ a * d ≤ c * b
    source
    theorem Rat.le_total {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 :
              Min ℚ
              Equations
                source
                instance Rat.instSup :
                Max ℚ
                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.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