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

source
def Rat.Nonneg (r : ℚ) :
Prop

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

Equations
Instances For
    source
    @[simp]
    theorem Rat.divInt_nonneg (a : ℤ) {b : ℤ} (h : 0 < b) :
    Rat.Nonneg (Rat.divInt a b) ↔ 0 ≤ a
    source
    theorem Rat.nonneg_add {a : ℚ} {b : ℚ} :
    Rat.Nonneg a → Rat.Nonneg b → Rat.Nonneg (a + b)
    source
    theorem Rat.nonneg_mul {a : ℚ} {b : ℚ} :
    Rat.Nonneg a → Rat.Nonneg b → Rat.Nonneg (a * b)
    source
    theorem Rat.nonneg_antisymm {a : ℚ} :
    Rat.Nonneg a → Rat.Nonneg (-a) → a = 0
    source
    theorem Rat.nonneg_total (a : ℚ) :
    Rat.Nonneg a ∨ Rat.Nonneg (-a)
    source
    instance Rat.decidableNonneg (a : ℚ) :
    Decidable (Rat.Nonneg a)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Rat.le' (a : ℚ) (b : ℚ) :
    Prop

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

    Equations
    Instances For
      source
      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
        source
        theorem Rat.le_iff_Nonneg (a : ℚ) (b : ℚ) :
        a ≤ b ↔ Rat.Nonneg (b - a)
        source
        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
        source
        theorem Rat.le_refl (a : ℚ) :
        a ≤ a
        source
        theorem Rat.le_total (a : ℚ) (b : ℚ) :
        a ≤ b ∨ b ≤ a
        source
        theorem Rat.le_antisymm {a : ℚ} {b : ℚ} (hab : a ≤ b) (hba : b ≤ a) :
        a = b
        source
        theorem Rat.le_trans {a : ℚ} {b : ℚ} {c : ℚ} (hab : a ≤ b) (hbc : b ≤ c) :
        a ≤ c
        source
        theorem Rat.not_le {a : ℚ} {b : ℚ} :
        ¬a ≤ b ↔ b < a
        source
        instance Rat.linearOrder :
        LinearOrder ℚ
        Equations
        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.nonneg_iff_zero_le {a : ℚ} :
        Rat.Nonneg a ↔ 0 ≤ a
        source
        theorem Rat.num_nonneg_iff_zero_le {a : ℚ} :
        0 ≤ a.num ↔ 0 ≤ a
        source
        theorem Rat.add_le_add_left {a : ℚ} {b : ℚ} {c : ℚ} :
        c + a ≤ c + b ↔ a ≤ b
        source
        theorem Rat.mul_nonneg {a : ℚ} {b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
        0 ≤ a * b
        source
        instance Rat.instLinearOrderedFieldRat :
        LinearOrderedField ℚ
        Equations
        • One or more equations did not get rendered due to their size.
        source
        instance Rat.instLinearOrderedCommRingRat :
        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
        theorem Rat.num_pos_iff_pos {a : ℚ} :
        0 < a.num ↔ 0 < a
        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