Documentation

Mathlib.Data.Rat.Order

Order for Rational Numbers #

Summary #

We define the order on , prove that is a discrete, linearly ordered field, and define functions such as abs and sqrt that depend on this order.

Tags #

rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering, sqrt, abs

def Rat.Nonneg (r : ) :

A rational number is called nonnegative if its numerator is nonnegative.

Equations
Instances For
    @[simp]
    theorem Rat.divInt_nonneg (a : ) {b : } (h : 0 < b) :
    theorem Rat.nonneg_add {a : } {b : } :
    Rat.Nonneg aRat.Nonneg bRat.Nonneg (a + b)
    theorem Rat.nonneg_mul {a : } {b : } :
    Rat.Nonneg aRat.Nonneg bRat.Nonneg (a * b)
    theorem Rat.nonneg_antisymm {a : } :
    Rat.Nonneg aRat.Nonneg (-a)a = 0
    Equations
    • One or more equations did not get rendered due to their size.
    def Rat.le' (a : ) (b : ) :

    Relation a ≤ b on defined as a ≤ b ↔ Rat.Nonneg (b - a). Use a ≤ b instead of Rat.le a b.

    Equations
    Instances For
      def Rat.numDenCasesOn'' {C : Sort u} (a : ) (H : (n : ) → (d : ) → (nz : d 0) → (red : Nat.Coprime (Int.natAbs n) d) → C (Rat.mk' n d)) :
      C a

      Define a (dependent) function or prove ∀ r : ℚ, p r by dealing with rational numbers of the form mk' n d with d ≠ 0.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Rat.le_iff_Nonneg (a : ) (b : ) :
        a b Rat.Nonneg (b - a)
        theorem Rat.le_def {a : } {b : } {c : } {d : } (b0 : 0 < b) (d0 : 0 < d) :
        Rat.divInt a b Rat.divInt c d a * d c * b
        theorem Rat.le_refl (a : ) :
        a a
        theorem Rat.le_total (a : ) (b : ) :
        a b b a
        theorem Rat.le_antisymm {a : } {b : } (hab : a b) (hba : b a) :
        a = b
        theorem Rat.le_trans {a : } {b : } {c : } (hab : a b) (hbc : b c) :
        a c
        theorem Rat.not_le {a : } {b : } :
        ¬a b b < a
        Equations
        Equations
        Equations
        Equations
        Equations
        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.num_nonneg_iff_zero_le {a : } :
        0 a.num 0 a
        theorem Rat.add_le_add_left {a : } {b : } {c : } :
        c + a c + b a b
        theorem Rat.mul_nonneg {a : } {b : } (ha : 0 a) (hb : 0 b) :
        0 a * b
        Equations
        • One or more equations did not get rendered due to their size.
        theorem Rat.num_pos_iff_pos {a : } :
        0 < a.num 0 < a
        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| = Rat.divInt (Int.natAbs q.num) q.den