doc-next-gen

Mathlib.Algebra.Order.Ring.Unbundled.Rat

Module docstring

{"# 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 ","### Extra instances to short-circuit type class resolution

These also prevent non-computable instances being used to construct these instances non-computably. ","### Miscellaneous lemmas "}

Rat.divInt_nonneg_iff_of_pos_right theorem
{a b : ℤ} (hb : 0 < b) : 0 ≤ a /. b ↔ 0 ≤ a
Full source 
@[simp] lemma divInt_nonneg_iff_of_pos_right {a b : ℤ} (hb : 0 < b) : 0 ≤ a /. b ↔ 0 ≤ a := by
  rcases hab : a /. b with ⟨n, d, hd, hnd⟩
  rw [mk'_eq_divInt, divInt_eq_iff hb.ne' (mod_cast hd)] at hab
  rw [← num_nonneg, ← Int.mul_nonneg_iff_of_pos_right hb, ← hab,
    Int.mul_nonneg_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero hd)]
Nonnegativity of Rational Fraction with Positive Denominator
Informal description
For any integers $a$ and $b$ with $b > 0$, the rational number $a / b$ is nonnegative if and only if $a$ is nonnegative, i.e., $0 \leq a / b \leftrightarrow 0 \leq a$.
Rat.divInt_nonneg theorem
{a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a /. b
Full source 
@[simp] lemma divInt_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a /. b := by
  obtain rfl | hb := hb.eq_or_lt
  · simp
    rfl
  rwa [divInt_nonneg_iff_of_pos_right hb]
Nonnegativity of Rational Fraction with Nonnegative Numerator and Denominator
Informal description
For any integers $a$ and $b$ such that $0 \leq a$ and $0 \leq b$, the rational number $a / b$ is nonnegative, i.e., $0 \leq a / b$.
Rat.mkRat_nonneg theorem
{a : ℤ} (ha : 0 ≤ a) (b : ℕ) : 0 ≤ mkRat a b
Full source 
@[simp] lemma mkRat_nonneg {a : ℤ} (ha : 0 ≤ a) (b : ℕ) : 0 ≤ mkRat a b := by
  simpa using divInt_nonneg ha (Int.natCast_nonneg _)
Nonnegativity of Rational Construction from Nonnegative Integer and Natural Number
Informal description
For any integer $a$ such that $0 \leq a$ and any natural number $b$, the rational number $\text{mkRat}(a, b)$ is nonnegative, i.e., $0 \leq \text{mkRat}(a, b)$.
Rat.ofScientific_nonneg theorem
(m : ℕ) (s : Bool) (e : ℕ) : 0 ≤ Rat.ofScientific m s e
Full source 
theorem ofScientific_nonneg (m : ℕ) (s : Bool) (e : ℕ) :
    0 ≤ Rat.ofScientific m s e := by
  rw [Rat.ofScientific]
  cases s
  · rw [if_neg (by decide)]
    refine num_nonneg.mp ?_
    rw [num_natCast]
    exact Int.natCast_nonneg _
  · rw [if_pos rfl, normalize_eq_mkRat]
    exact Rat.mkRat_nonneg (Int.natCast_nonneg _) _
Nonnegativity of Rational Numbers in Scientific Notation
Informal description
For any natural numbers $m$ and $e$, and any boolean $s$, the rational number constructed via scientific notation $\text{ofScientific}(m, s, e)$ is nonnegative, i.e., $0 \leq \text{ofScientific}(m, s, e)$.
NNRatCast.toOfScientific instance
{K} [NNRatCast K] : OfScientific K
Full source 
instance _root_.NNRatCast.toOfScientific {K} [NNRatCast K] : OfScientific K where
  ofScientific (m : ℕ) (b : Bool) (d : ℕ) :=
    NNRat.cast ⟨Rat.ofScientific m b d, ofScientific_nonneg m b d⟩
Scientific Notation for Types with Nonnegative Rational Embedding
Informal description
For any type $K$ with a canonical homomorphism from nonnegative rationals, $K$ inherits the structure of a type that can represent numbers in scientific notation.
NNRat.cast_ofScientific theorem
{K} [NNRatCast K] (m : ℕ) (s : Bool) (e : ℕ) : (OfScientific.ofScientific m s e : ℚ≥0) = (OfScientific.ofScientific m s e : K)
Full source 
/-- Casting a scientific literal via `ℚ≥0` is the same as casting directly. -/
@[simp, norm_cast]
theorem _root_.NNRat.cast_ofScientific {K} [NNRatCast K] (m : ℕ) (s : Bool) (e : ℕ) :
    (OfScientific.ofScientific m s e : ℚ≥0) = (OfScientific.ofScientific m s e : K) :=
  rfl
Equality of Scientific Notation Casts via Nonnegative Rationals
Informal description
For any type $K$ with a canonical homomorphism from nonnegative rationals, and for any natural numbers $m$, $e$ and boolean $s$, the scientific notation $\text{ofScientific}(m, s, e)$ yields the same element in $\mathbb{Q}_{\geq 0}$ and in $K$ under the canonical homomorphism. That is, $$(\text{ofScientific}(m, s, e) : \mathbb{Q}_{\geq 0}) = (\text{ofScientific}(m, s, e) : K).$$
Rat.add_nonneg theorem
: 0 ≤ a → 0 ≤ b → 0 ≤ a + b
Full source 
protected lemma add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b :=
  numDenCasesOn' a fun n₁ d₁ h₁ ↦ numDenCasesOn' b fun n₂ d₂ h₂ ↦ by
    have d₁0 : 0 < (d₁ : ℤ) := mod_cast Nat.pos_of_ne_zero h₁
    have d₂0 : 0 < (d₂ : ℤ) := mod_cast Nat.pos_of_ne_zero h₂
    simp only [d₁0, d₂0, h₁, h₂, Int.mul_pos, divInt_nonneg_iff_of_pos_right, divInt_add_divInt, Ne,
      Nat.cast_eq_zero, not_false_iff]
    intro n₁0 n₂0
    apply Int.add_nonneg <;> apply Int.mul_nonneg <;> · first | assumption | apply Int.ofNat_zero_le
Nonnegativity of Sum of Nonnegative Rationals
Informal description
For any rational numbers $a$ and $b$, if $0 \leq a$ and $0 \leq b$, then $0 \leq a + b$.
Rat.mul_nonneg theorem
: 0 ≤ a → 0 ≤ b → 0 ≤ a * b
Full source 
protected lemma mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
  numDenCasesOn' a fun n₁ d₁ h₁ =>
    numDenCasesOn' b fun n₂ d₂ h₂ => by
      have d₁0 : 0 < (d₁ : ℤ) := mod_cast Nat.pos_of_ne_zero h₁
      have d₂0 : 0 < (d₂ : ℤ) := mod_cast Nat.pos_of_ne_zero h₂
      simp only [d₁0, d₂0, Int.mul_pos, divInt_nonneg_iff_of_pos_right,
        divInt_mul_divInt _ _ d₁0.ne' d₂0.ne']
      apply Int.mul_nonneg
Nonnegativity of Product of Nonnegative Rationals
Informal description
For any rational numbers $a$ and $b$, if $0 \leq a$ and $0 \leq b$, then $0 \leq a \cdot b$.
Rat.not_le theorem
{a b : ℚ} : ¬a ≤ b ↔ b < a
Full source 
protected theorem not_le {a b : ℚ} : ¬a ≤ b¬a ≤ b ↔ b < a := (Bool.not_eq_false _).to_iff
Negation of Rational Order: $\neg (a \leq b) \leftrightarrow b < a$
Informal description
For any two rational numbers $a$ and $b$, the statement $\neg (a \leq b)$ is equivalent to $b < a$.
Rat.not_lt theorem
{a b : ℚ} : ¬a < b ↔ b ≤ a
Full source 
protected theorem not_lt {a b : ℚ} : ¬a < b¬a < b ↔ b ≤ a := by
  rw [← Rat.not_le, not_not]
Negation of Rational Strict Order: $\neg (a < b) \leftrightarrow b \leq a$
Informal description
For any two rational numbers $a$ and $b$, the statement $\neg (a < b)$ is equivalent to $b \leq a$.
Rat.lt_iff theorem
(a b : ℚ) : a < b ↔ a.num * b.den < b.num * a.den
Full source 
protected theorem lt_iff (a b : ℚ) : a < b ↔ a.num * b.den < b.num * a.den :=
  numDenCasesOn'' a fun na da ha hared =>
    numDenCasesOn'' b fun nb db hb hbred => by
      show Rat.bltRat.blt _ _ = true ↔ _
      suffices
        (na < 0 ∧ 0 ≤ nb ∨ if na = 0 then 0 < nb else (na ≤ 0 ∨ 0 < nb) ∧ na * ↑db < nb * da) ↔
        na * db < nb * da by simpa [Rat.blt]
      split_ifs with h
      · suffices 0 < nb ↔ 0 < nb * da by simpa [h]
        refine ⟨(Int.mul_pos · (by omega)), ?_⟩
        contrapose!
        exact (Int.mul_nonpos_of_nonpos_of_nonneg · (by omega))
      · constructor
        · refine (·.elim ?_ And.right)
          rintro ⟨hna, nb0⟩
          apply (Int.mul_neg_of_neg_of_pos hna _).trans_le (Int.mul_nonneg nb0 _) <;> omega
        · intro h
          suffices na < 0 ∧ 0 ≤ nbna < 0 ∧ 0 ≤ nb ∨ na ≤ 0 ∨ 0 < nb by simpa [h]
          contrapose! h
          apply (Int.mul_nonpos_of_nonpos_of_nonneg _ _).trans (Int.mul_nonneg _ _) <;> omega
Rational Order Criterion via Cross-Multiplication: $a < b \leftrightarrow \text{num}(a)\text{den}(b) < \text{num}(b)\text{den}(a)$
Informal description
For any two rational numbers $a$ and $b$, the strict inequality $a < b$ holds if and only if the product of the numerator of $a$ and the denominator of $b$ is strictly less than the product of the numerator of $b$ and the denominator of $a$, i.e., $a < b \leftrightarrow \text{num}(a) \cdot \text{den}(b) < \text{num}(b) \cdot \text{den}(a)$.
Rat.le_iff theorem
(a b : ℚ) : a ≤ b ↔ a.num * b.den ≤ b.num * a.den
Full source 
protected theorem le_iff (a b : ℚ) : a ≤ b ↔ a.num * b.den ≤ b.num * a.den := by
  simpa only [Rat.not_lt, not_lt] using (Rat.lt_iff b a).not
Rational Order Criterion via Cross-Multiplication: $a \leq b \leftrightarrow \text{num}(a)\text{den}(b) \leq \text{num}(b)\text{den}(a)$
Informal description
For any two rational numbers $a$ and $b$, the inequality $a \leq b$ holds if and only if the product of the numerator of $a$ and the denominator of $b$ is less than or equal to the product of the numerator of $b$ and the denominator of $a$, i.e., $a \leq b \leftrightarrow \text{num}(a) \cdot \text{den}(b) \leq \text{num}(b) \cdot \text{den}(a)$.
Rat.le_iff_sub_nonneg theorem
(a b : ℚ) : a ≤ b ↔ 0 ≤ b - a
Full source 
protected theorem le_iff_sub_nonneg (a b : ℚ) : a ≤ b ↔ 0 ≤ b - a :=
  numDenCasesOn'' a fun na da ha hared =>
    numDenCasesOn'' b fun nb db hb hbred => by
      rw [Rat.le_iff, sub_def, normalize_eq, ← num_nonneg, ← Int.sub_nonneg]
      dsimp only
      refine ⟨(Int.ediv_nonneg · (Int.natCast_nonneg _)), fun H ↦ ?_⟩
      contrapose! H
      apply Int.ediv_neg_of_neg_of_pos H
      simp only [Int.natCast_pos, Nat.pos_iff_ne_zero]
      exact Nat.gcd_ne_zero_right (Nat.mul_ne_zero hb ha)
Rational Order Criterion via Nonnegative Difference: $a \leq b \leftrightarrow 0 \leq b - a$
Informal description
For any two rational numbers $a$ and $b$, the inequality $a \leq b$ holds if and only if their difference $b - a$ is nonnegative, i.e., $0 \leq b - a$.
Rat.divInt_le_divInt theorem
{a b c d : ℤ} (b0 : 0 < b) (d0 : 0 < d) : a /. b ≤ c /. d ↔ a * d ≤ c * b
Full source 
protected lemma divInt_le_divInt {a b c d : ℤ} (b0 : 0 < b) (d0 : 0 < d) :
    a /. ba /. b ≤ c /. d ↔ a * d ≤ c * b := by
  rw [Rat.le_iff_sub_nonneg, ← Int.sub_nonneg]
  simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, Int.mul_pos d0 b0]
Cross-Multiplication Inequality for Rational Numbers: $\frac{a}{b} \leq \frac{c}{d} \leftrightarrow a \cdot d \leq c \cdot b$
Informal description
For integers $a, b, c, d$ with $b > 0$ and $d > 0$, the rational number $\frac{a}{b}$ is less than or equal to $\frac{c}{d}$ if and only if $a \cdot d \leq c \cdot b$.
Rat.linearOrder instance
: LinearOrder ℚ
Full source 
instance linearOrder : LinearOrder ℚ where
  le_refl a := by rw [Rat.le_iff_sub_nonneg, ← num_nonneg]; simp
  le_trans a b c hab hbc := by
    rw [Rat.le_iff_sub_nonneg] at hab hbc
    have := Rat.add_nonneg hab hbc
    simp_rw [sub_eq_add_neg, add_left_comm (b + -a) c (-b), add_comm (b + -a) (-b),
      add_left_comm (-b) b (-a), add_comm (-b) (-a), add_neg_cancel_comm_assoc,
      ← sub_eq_add_neg] at this
    rwa [Rat.le_iff_sub_nonneg]
  le_antisymm a b hab hba := by
    rw [Rat.le_iff_sub_nonneg] at hab hba
    rw [sub_eq_add_neg] at hba
    rw [← neg_sub, sub_eq_add_neg] at hab
    have := eq_neg_of_add_eq_zero_left (Rat.nonneg_antisymm hba hab)
    rwa [neg_neg] at this
  le_total _ _ := Rat.le_total
  toDecidableEq := inferInstance
  toDecidableLE := inferInstance
  toDecidableLT := inferInstance
  lt_iff_le_not_le _ _ := by rw [← Rat.not_le, and_iff_right_of_imp Rat.le_total.resolve_left]
Linear Order on Rational Numbers
Informal description
The rational numbers $\mathbb{Q}$ form a linear order.
Rat.instDistribLattice instance
: DistribLattice ℚ
Full source 
instance instDistribLattice : DistribLattice ℚ := inferInstance
Distributive Lattice Structure on Rational Numbers
Informal description
The rational numbers $\mathbb{Q}$ form a distributive lattice, where the join and meet operations are given by the maximum and minimum operations respectively.
Rat.instLattice instance
: Lattice ℚ
Full source 
instance instLattice : Lattice ℚ := inferInstance
The Lattice Structure on Rational Numbers
Informal description
The rational numbers $\mathbb{Q}$ form a lattice, where the join and meet operations are given by the maximum and minimum operations respectively.
Rat.instSemilatticeInf instance
: SemilatticeInf ℚ
Full source 
instance instSemilatticeInf : SemilatticeInf ℚ := inferInstance
The Meet-Semilattice Structure on Rational Numbers
Informal description
The rational numbers $\mathbb{Q}$ form a meet-semilattice, where the meet operation is given by the minimum operation.
Rat.instSemilatticeSup instance
: SemilatticeSup ℚ
Full source 
instance instSemilatticeSup : SemilatticeSup ℚ := inferInstance
Join-Semilattice Structure on Rational Numbers
Informal description
The rational numbers $\mathbb{Q}$ form a join-semilattice, where the join operation is given by the maximum operation.
Rat.instInf instance
: Min ℚ
Full source 
instance instInf : Min ℚ := inferInstance
Minimum Operation on Rational Numbers
Informal description
The rational numbers $\mathbb{Q}$ have a minimum operation.
Rat.instSup instance
: Max ℚ
Full source 
instance instSup : Max ℚ := inferInstance
Maximum Operation on Rational Numbers
Informal description
The rational numbers $\mathbb{Q}$ have a maximum operation.
Rat.instPartialOrder instance
: PartialOrder ℚ
Full source 
instance instPartialOrder : PartialOrder ℚ := inferInstance
Partial Order Structure on Rational Numbers
Informal description
The rational numbers $\mathbb{Q}$ form a partial order, where the order relation is defined by $p \leq q$ if and only if $p_{\text{num}} \cdot q_{\text{den}} \leq q_{\text{num}} \cdot p_{\text{den}}$, where $p_{\text{num}}$ and $p_{\text{den}}$ are the numerator and denominator of $p$ respectively (and similarly for $q$).
Rat.instPreorder instance
: Preorder ℚ
Full source 
instance instPreorder : Preorder ℚ := inferInstance
Preorder Structure on Rational Numbers
Informal description
The rational numbers $\mathbb{Q}$ form a preorder, where the order relation is defined by $p \leq q$ if and only if $p_{\text{num}} \cdot q_{\text{den}} \leq q_{\text{num}} \cdot p_{\text{den}}$, where $p_{\text{num}}$ and $p_{\text{den}}$ are the numerator and denominator of $p$ respectively (and similarly for $q$).
Rat.le_def theorem
: p ≤ q ↔ p.num * q.den ≤ q.num * p.den
Full source 
protected lemma le_def : p ≤ q ↔ p.num * q.den ≤ q.num * p.den := by
  rw [← num_divInt_den q, ← num_divInt_den p]
  conv_rhs => simp only [num_divInt_den]
  exact Rat.divInt_le_divInt (mod_cast p.pos) (mod_cast q.pos)
Characterization of Order on Rational Numbers via Cross-Multiplication
Informal description
For any rational numbers $p$ and $q$, the inequality $p \leq q$ holds if and only if the product of the numerator of $p$ and the denominator of $q$ is less than or equal to the product of the numerator of $q$ and the denominator of $p$, i.e., $\text{num}(p) \cdot \text{den}(q) \leq \text{num}(q) \cdot \text{den}(p)$.
Rat.lt_def theorem
: p < q ↔ p.num * q.den < q.num * p.den
Full source 
protected lemma lt_def : p < q ↔ p.num * q.den < q.num * p.den := by
  rw [lt_iff_le_and_ne, Rat.le_def]
  suffices p ≠ qp ≠ q ↔ p.num * q.den ≠ q.num * p.den by
    constructor <;> intro h
    · exact lt_iff_le_and_ne.mpr ⟨h.left, this.mp h.right⟩
    · have tmp := lt_iff_le_and_ne.mp h
      exact ⟨tmp.left, this.mpr tmp.right⟩
  exact not_iff_not.mpr eq_iff_mul_eq_mul
Characterization of Strict Order on Rational Numbers via Cross-Multiplication
Informal description
For any rational numbers $p$ and $q$, the strict inequality $p < q$ holds if and only if the product of the numerator of $p$ and the denominator of $q$ is strictly less than the product of the numerator of $q$ and the denominator of $p$, i.e., $\text{num}(p) \cdot \text{den}(q) < \text{num}(q) \cdot \text{den}(p)$.
Rat.instAddLeftMono instance
: AddLeftMono ℚ
Full source 
instance : AddLeftMono ℚ where
  elim := fun _ _ _ h => Rat.add_le_add_left.2 h
Addition is Monotone in Rational Numbers
Informal description
For any rational number $c$, the function $a \mapsto c + a$ is monotone (order-preserving) with respect to the order on $\mathbb{Q}$.
Rat.num_nonpos theorem
{a : ℚ} : a.num ≤ 0 ↔ a ≤ 0
Full source 
@[simp] lemma num_nonpos {a : ℚ} : a.num ≤ 0 ↔ a ≤ 0 := by
  simp [Int.le_iff_lt_or_eq, instLE, Rat.blt, Int.not_lt]
Nonpositivity of Rational Number and Its Numerator
Informal description
For any rational number $a$, the numerator of $a$ is nonpositive if and only if $a$ is nonpositive, i.e., $\text{num}(a) \leq 0 \leftrightarrow a \leq 0$.
Rat.num_pos theorem
{a : ℚ} : 0 < a.num ↔ 0 < a
Full source 
@[simp] lemma num_pos {a : ℚ} : 0 < a.num ↔ 0 < a := lt_iff_lt_of_le_iff_le num_nonpos
Positivity of Rational Number and Its Numerator
Informal description
For any rational number $a$, the numerator of $a$ is positive if and only if $a$ itself is positive, i.e., $\text{num}(a) > 0 \leftrightarrow a > 0$.
Rat.num_neg theorem
{a : ℚ} : a.num < 0 ↔ a < 0
Full source 
@[simp] lemma num_neg {a : ℚ} : a.num < 0 ↔ a < 0 := lt_iff_lt_of_le_iff_le num_nonneg
Negativity of Rational Number and Its Numerator
Informal description
For any rational number $a$, the numerator of $a$ is negative if and only if $a$ itself is negative, i.e., $\text{num}(a) < 0 \leftrightarrow a < 0$.
Rat.div_lt_div_iff_mul_lt_mul theorem
{a b c d : ℤ} (b_pos : 0 < b) (d_pos : 0 < d) : (a : ℚ) / b < c / d ↔ a * d < c * b
Full source 
theorem 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 := by
  simp only [lt_iff_le_not_le]
  apply and_congr
  · simp [div_def', Rat.divInt_le_divInt b_pos d_pos]
  · apply not_congr
    simp [div_def', Rat.divInt_le_divInt d_pos b_pos]
Cross-Multiplication Strict Inequality for Rational Numbers: $\frac{a}{b} < \frac{c}{d} \leftrightarrow a \cdot d < c \cdot b$
Informal description
For integers $a, b, c, d$ with $b > 0$ and $d > 0$, the rational number $\frac{a}{b}$ is strictly less than $\frac{c}{d}$ if and only if $a \cdot d < c \cdot b$.
Rat.lt_one_iff_num_lt_denom theorem
{q : ℚ} : q < 1 ↔ q.num < q.den
Full source 
theorem lt_one_iff_num_lt_denom {q : ℚ} : q < 1 ↔ q.num < q.den := by simp [Rat.lt_def]
Rational Number Less Than One iff Numerator Less Than Denominator
Informal description
For any rational number $q$, we have $q < 1$ if and only if the numerator of $q$ is less than its denominator.
Rat.abs_def theorem
(q : ℚ) : |q| = q.num.natAbs /. q.den
Full source 
theorem abs_def (q : ℚ) : |q| = q.num.natAbs /. q.den := by
  rcases le_total q 0 with hq | hq
  · rw [abs_of_nonpos hq]
    rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt (mod_cast q.pos) Int.zero_lt_one,
      mul_one, zero_mul] at hq
    rw [Int.ofNat_natAbs_of_nonpos hq, ← neg_def]
  · rw [abs_of_nonneg hq]
    rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt Int.zero_lt_one (mod_cast q.pos),
      mul_one, zero_mul] at hq
    rw [Int.natAbs_of_nonneg hq, num_divInt_den]
Absolute Value of Rational Number as Fraction of Absolute Numerator and Denominator
Informal description
For any rational number $q$, the absolute value of $q$ is equal to the fraction formed by the absolute value of its numerator and its denominator, i.e., $|q| = \frac{|\text{num}(q)|}{\text{den}(q)}$.