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

def Rat.Nonneg (r : ℚ) :

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

Equations

Rat.Nonneg r = (0 ≤ r.num)

Instances For

Rat.decidableNonneg

@[simp]

theorem Rat.divInt_nonneg (a : ℤ) {b : ℤ} (h : 0 < b) :

Rat.Nonneg (Rat.divInt a b) ↔ 0 ≤ a

theorem Rat.nonneg_add {a : ℚ} {b : ℚ} :

Rat.Nonneg a → Rat.Nonneg b → Rat.Nonneg (a + b)

theorem Rat.nonneg_mul {a : ℚ} {b : ℚ} :

Rat.Nonneg a → Rat.Nonneg b → Rat.Nonneg (a * b)

theorem Rat.nonneg_antisymm {a : ℚ} :

Rat.Nonneg a → Rat.Nonneg (-a) → a = 0

theorem Rat.nonneg_total (a : ℚ) :

Rat.Nonneg a ∨ Rat.Nonneg (-a)

instance Rat.decidableNonneg (a : ℚ) :

Decidable (Rat.Nonneg a)

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

Rat.le' a b = Rat.Nonneg (b - a)

def Rat.numDenCasesOn'' {C : ℚ → Sort u} (a : ℚ) (H : (n : ℤ) → (d : ℕ) → (nz : d ≠ 0) → (red : Nat.Coprime (Int.natAbs n) d) → C { num := n, den := d, den_nz := nz, reduced := red }) :

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

Rat.numDenCasesOn'' a H = Rat.numDenCasesOn a fun (n : ℤ) (d : ℕ) (h : 0 < d) (h' : Nat.Coprime (Int.natAbs n) d) => Eq.mpr ⋯ (H n d ⋯ h')

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

instance Rat.linearOrder :

LinearOrder ℚ

Equations

One or more equations did not get rendered due to their size.

instance Rat.instLTRat_1 :

Equations

Rat.instLTRat_1 = inferInstance

instance Rat.instDistribLatticeRat :

DistribLattice ℚ

Equations

Rat.instDistribLatticeRat = inferInstance

instance Rat.instLatticeRat :

Equations

Rat.instLatticeRat = inferInstance

instance Rat.instSemilatticeInfRat :

SemilatticeInf ℚ

Equations

Rat.instSemilatticeInfRat = inferInstance

instance Rat.instSemilatticeSupRat :

SemilatticeSup ℚ

Equations

Rat.instSemilatticeSupRat = inferInstance

instance Rat.instInfRat :

Equations

Rat.instInfRat = inferInstance

instance Rat.instSupRat :

Equations

Rat.instSupRat = inferInstance

instance Rat.instPartialOrderRat :

PartialOrder ℚ

Equations

Rat.instPartialOrderRat = inferInstance

instance Rat.instPreorderRat :

Equations

Rat.instPreorderRat = inferInstance

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.nonneg_iff_zero_le {a : ℚ} :

Rat.Nonneg a ↔ 0 ≤ a

@[simp]

theorem Rat.num_nonneg {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

instance Rat.instLinearOrderedCommRing :

LinearOrderedCommRing ℚ

Equations

Rat.instLinearOrderedCommRing = let __spread.0 := Rat.linearOrder; let __spread.1 := Rat.commRing; LinearOrderedCommRing.mk ⋯

instance Rat.instLinearOrderedRingRat :

LinearOrderedRing ℚ

Equations

Rat.instLinearOrderedRingRat = inferInstance

instance Rat.instOrderedRingRat :

OrderedRing ℚ

Equations

Rat.instOrderedRingRat = inferInstance

instance Rat.instLinearOrderedSemiringRat :

LinearOrderedSemiring ℚ

Equations

Rat.instLinearOrderedSemiringRat = inferInstance

instance Rat.instOrderedSemiringRat :

OrderedSemiring ℚ

Equations

Rat.instOrderedSemiringRat = inferInstance

instance Rat.instLinearOrderedAddCommGroupRat :

LinearOrderedAddCommGroup ℚ

Equations

Rat.instLinearOrderedAddCommGroupRat = inferInstance

instance Rat.instOrderedAddCommGroupRat :

OrderedAddCommGroup ℚ

Equations

Rat.instOrderedAddCommGroupRat = inferInstance

instance Rat.instOrderedCancelAddCommMonoidRat :

OrderedCancelAddCommMonoid ℚ

Equations

Rat.instOrderedCancelAddCommMonoidRat = inferInstance

instance Rat.instOrderedAddCommMonoidRat :

OrderedAddCommMonoid ℚ

Equations

Rat.instOrderedAddCommMonoidRat = inferInstance

@[simp]

theorem Rat.num_nonpos {a : ℚ} :

a.num ≤ 0 ↔ a ≤ 0

@[simp]

theorem Rat.num_pos {a : ℚ} :

0 < a.num ↔ 0 < a

@[simp]

theorem Rat.num_neg {a : ℚ} :

a.num < 0 ↔ a < 0

@[deprecated Rat.num_nonneg]

theorem Rat.num_nonneg_iff_zero_le {a : ℚ} :

0 ≤ a.num ↔ 0 ≤ a

Alias of Rat.num_nonneg.

@[deprecated Rat.num_pos]

theorem Rat.num_pos_iff_pos {a : ℚ} :

0 < a.num ↔ 0 < a

Alias of Rat.num_pos.

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