doc-next-gen

Mathlib.Algebra.Field.Rat

Module docstring

{"# The rational numbers form a field

This file contains the field instance on the rational numbers.

See note [foundational algebra order theory].

Tags

rat, rationals, field, ℚ, numerator, denominator, num, denom ","### Extra instances to short-circuit type class resolution

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

Rat.instDivisionRing instance
: DivisionRing ℚ
Full source 
instance instDivisionRing : DivisionRing ℚ := inferInstance
The Division Ring Structure on Rational Numbers
Informal description
The rational numbers $\mathbb{Q}$ form a division ring.
Rat.inv_nonneg theorem
{a : ℚ} (ha : 0 ≤ a) : 0 ≤ a⁻¹
Full source 
protected lemma inv_nonneg {a : ℚ} (ha : 0 ≤ a) : 0 ≤ a⁻¹ := by
  rw [inv_def']
  exact divInt_nonneg (Int.ofNat_nonneg a.den) (num_nonneg.mpr ha)
Nonnegativity of the Inverse of a Nonnegative Rational Number
Informal description
For any nonnegative rational number $a$ (i.e., $0 \leq a$), its multiplicative inverse $a^{-1}$ is also nonnegative, i.e., $0 \leq a^{-1}$.
Rat.div_nonneg theorem
{a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b
Full source 
protected lemma div_nonneg {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b :=
  mul_nonneg ha (Rat.inv_nonneg hb)
Nonnegativity of the Quotient of Nonnegative Rational Numbers
Informal description
For any nonnegative rational numbers $a$ and $b$ (i.e., $0 \leq a$ and $0 \leq b$), their quotient $a / b$ is also nonnegative, i.e., $0 \leq a / b$.
Rat.zpow_nonneg theorem
{a : ℚ} (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
Full source 
protected lemma zpow_nonneg {a : ℚ} (ha : 0 ≤ a) : ∀ n : ℤ, 0 ≤ a ^ n
  | Int.ofNat n => by simp [ha]
  | Int.negSucc n => by simpa using Rat.inv_nonneg (pow_nonneg ha (n + 1))
Nonnegativity of Integer Powers of Nonnegative Rationals
Informal description
For any nonnegative rational number $a$ (i.e., $0 \leq a$) and any integer $n$, the $n$-th power of $a$ is nonnegative, i.e., $a^n \geq 0$.
NNRat.instInv instance
: Inv ℚ≥0
Full source 
instance instInv : Inv ℚ≥0 where
  inv x := ⟨x⁻¹, Rat.inv_nonneg x.2⟩
Inversion Operation on Nonnegative Rational Numbers
Informal description
The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ are equipped with an inversion operation.
NNRat.instDiv instance
: Div ℚ≥0
Full source 
instance instDiv : Div ℚ≥0 where
  div x y := ⟨x / y, Rat.div_nonneg x.2 y.2⟩
Division Operation on Nonnegative Rational Numbers
Informal description
The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ are equipped with a division operation.
NNRat.instZPow instance
: Pow ℚ≥0 ℤ
Full source 
instance instZPow : Pow ℚ≥0 ℤ where
  pow x n := ⟨x ^ n, Rat.zpow_nonneg x.2 n⟩
Integer Powers on Nonnegative Rational Numbers
Informal description
The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ are equipped with an integer power operation $q^n$ for $q \in \mathbb{Q}_{\geq 0}$ and $n \in \mathbb{Z}$.
NNRat.coe_inv theorem
(q : ℚ≥0) : ((q⁻¹ : ℚ≥0) : ℚ) = (q : ℚ)⁻¹
Full source 
@[simp, norm_cast] lemma coe_inv (q : ℚ≥0) : ((q⁻¹ : ℚ≥0) : ℚ) = (q : ℚ)⁻¹ := rfl
Embedding Preserves Inversion of Nonnegative Rationals: $(q^{-1}) = q^{-1}$
Informal description
For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the canonical embedding of its inverse in $\mathbb{Q}_{\geq 0}$ into the rational numbers $\mathbb{Q}$ equals the inverse of its embedding, i.e., $(q^{-1} : \mathbb{Q}) = (q : \mathbb{Q})^{-1}$.
NNRat.coe_div theorem
(p q : ℚ≥0) : ((p / q : ℚ≥0) : ℚ) = p / q
Full source 
@[simp, norm_cast] lemma coe_div (p q : ℚ≥0) : ((p / q : ℚ≥0) : ℚ) = p / q := rfl
Embedding Preserves Division of Nonnegative Rationals: $(p / q) = p / q$
Informal description
For any nonnegative rational numbers $p$ and $q$, the canonical embedding of their quotient in $\mathbb{Q}_{\geq 0}$ into the rational numbers $\mathbb{Q}$ equals the quotient of their embeddings, i.e., $(p / q : \mathbb{Q}) = (p : \mathbb{Q}) / (q : \mathbb{Q})$.
NNRat.coe_zpow theorem
(p : ℚ≥0) (n : ℤ) : ((p ^ n : ℚ≥0) : ℚ) = p ^ n
Full source 
@[simp, norm_cast] lemma coe_zpow (p : ℚ≥0) (n : ℤ) : ((p ^ n : ℚ≥0) : ℚ) = p ^ n := rfl
Embedding Preserves Integer Powers of Nonnegative Rationals: $(p^n) = p^n$
Informal description
For any nonnegative rational number $p \in \mathbb{Q}_{\geq 0}$ and any integer $n \in \mathbb{Z}$, the canonical embedding of the $n$-th power of $p$ in $\mathbb{Q}_{\geq 0}$ into the rational numbers $\mathbb{Q}$ equals the $n$-th power of the embedding of $p$, i.e., $(p^n : \mathbb{Q}) = (p : \mathbb{Q})^n$.
NNRat.inv_def theorem
(q : ℚ≥0) : q⁻¹ = divNat q.den q.num
Full source 
lemma inv_def (q : ℚ≥0) : q⁻¹ = divNat q.den q.num := by ext; simp [Rat.inv_def', num_coe, den_coe]
Inverse of Nonnegative Rational as Denominator over Numerator: $q^{-1} = \text{den}(q)/\text{num}(q)$
Informal description
For any nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the inverse $q^{-1}$ is equal to the quotient of its denominator and numerator as natural numbers, i.e., $q^{-1} = \frac{\text{den}(q)}{\text{num}(q)}$.
NNRat.div_def theorem
(p q : ℚ≥0) : p / q = divNat (p.num * q.den) (p.den * q.num)
Full source 
lemma div_def (p q : ℚ≥0) : p / q = divNat (p.num * q.den) (p.den * q.num) := by
  ext; simp [Rat.div_def', num_coe, den_coe]
Division Formula for Nonnegative Rational Numbers: $p / q = \frac{\text{num}(p) \cdot \text{den}(q)}{\text{den}(p) \cdot \text{num}(q)}$
Informal description
For any two nonnegative rational numbers $p$ and $q$, their division $p / q$ is equal to the nonnegative rational number constructed as the quotient of the product of the numerator of $p$ and the denominator of $q$ over the product of the denominator of $p$ and the numerator of $q$, i.e., $$ p / q = \frac{\text{num}(p) \cdot \text{den}(q)}{\text{den}(p) \cdot \text{num}(q)}. $$
NNRat.num_inv_of_ne_zero theorem
{q : ℚ≥0} (hq : q ≠ 0) : q⁻¹.num = q.den
Full source 
lemma num_inv_of_ne_zero {q : ℚ≥0} (hq : q ≠ 0) : q⁻¹.num = q.den := by
  rw [inv_def, divNat, num, coe_mk, Rat.divInt_ofNat, ← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq),
    Int.natAbs_natCast]
  simpa using q.coprime_num_den.symm
Numerator of Inverse Equals Denominator for Nonzero Nonnegative Rationals: $\text{num}(q^{-1}) = \text{den}(q)$
Informal description
For any nonzero nonnegative rational number $q \in \mathbb{Q}_{\geq 0}$, the numerator of the inverse $q^{-1}$ is equal to the denominator of $q$, i.e., $\text{num}(q^{-1}) = \text{den}(q)$.
NNRat.den_inv_of_ne_zero theorem
{q : ℚ≥0} (hq : q ≠ 0) : q⁻¹.den = q.num
Full source 
lemma den_inv_of_ne_zero {q : ℚ≥0} (hq : q ≠ 0) : q⁻¹.den = q.num := by
  rw [inv_def, divNat, den, coe_mk, Rat.divInt_ofNat, ← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq)]
  simpa using q.coprime_num_den.symm
Denominator of Inverse Equals Numerator for Nonzero Nonnegative Rationals
Informal description
For any nonzero nonnegative rational number $q$, the denominator of its inverse $q^{-1}$ is equal to the numerator of $q$, i.e., $\text{den}(q^{-1}) = \text{num}(q)$.
NNRat.num_div_den theorem
(q : ℚ≥0) : (q.num : ℚ≥0) / q.den = q
Full source 
@[simp]
lemma num_div_den (q : ℚ≥0) : (q.num : ℚ≥0) / q.den = q := by
  ext1
  rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_natCast]
  exact (cast_def _).symm
Nonnegative Rational as Quotient of Numerator and Denominator: $\frac{q_{\text{num}}}{q_{\text{den}}} = q$
Informal description
For any nonnegative rational number $q$, the quotient of its numerator (as a nonnegative rational number) and its denominator equals $q$ itself, i.e., $\frac{q_{\text{num}}}{q_{\text{den}}} = q$.
NNRat.instSemifield instance
: Semifield ℚ≥0
Full source 
instance instSemifield : Semifield ℚ≥0 where
  __ := instNNRatCommSemiring
  inv_zero := by ext; simp
  mul_inv_cancel q h := by ext; simp [h]
  nnratCast_def q := q.num_div_den.symm
  nnqsmul q a := q * a
  nnqsmul_def q a := rfl
  zpow n a := a ^ n
  zpow_zero' a := by ext; norm_cast
  zpow_succ' n a := by ext; norm_cast
  zpow_neg' n a := by ext; norm_cast
Nonnegative Rationals as a Commutative Division Semiring
Informal description
The nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ form a commutative division semiring.