Documentation

Mathlib.Algebra.Field.Rat

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

source
🔸 coverage
@[implicit_reducible]
instance Rat.instField :
Field ℚ

Extra instances to short-circuit type class resolution #

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

source
🔸 coverage
@[implicit_reducible]
instance Rat.instDivisionRing :
DivisionRing ℚ
source
theorem Rat.inv_nonneg {a : ℚ} (ha : 0 ≤ a) :
0 ≤ a⁻¹
source
theorem Rat.div_nonneg {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ a / b
source
🔸 coverage
@[implicit_reducible]
instance NNRat.instInv :
Inv ℚ≥0
source
🔸 coverage
@[implicit_reducible]
instance NNRat.instDiv :
Div ℚ≥0
source
🔸 coverage
@[implicit_reducible]
instance NNRat.instZPow :
Pow ℚ≥0 ℤ
source
📐 coverage
@[simp]
theorem NNRat.coe_inv (q : ℚ≥0) :
↑q⁻¹ = (↑q)⁻¹
source
📐 coverage
@[simp]
theorem NNRat.coe_div (p q : ℚ≥0) :
↑(p / q) = ↑p / ↑q
source
📐 coverage
@[simp]
theorem NNRat.coe_zpow (p : ℚ≥0) (n : ℤ) :
↑(p ^ n) = ↑p ^ n
source
📐 coverage
theorem NNRat.inv_def (q : ℚ≥0) :
q⁻¹ = divNat q.den q.num
source
📐 coverage
theorem NNRat.div_def (p q : ℚ≥0) :
p / q = divNat (p.num * q.den) (p.den * q.num)
source
📐 coverage
theorem NNRat.num_inv_of_ne_zero {q : ℚ≥0} (hq : q ≠ 0) :
q⁻¹.num = q.den
source
📐 coverage
theorem NNRat.den_inv_of_ne_zero {q : ℚ≥0} (hq : q ≠ 0) :
q⁻¹.den = q.num
source
📐 coverage
@[simp]
theorem NNRat.num_div_den (q : ℚ≥0) :
↑q.num / ↑q.den = q
source
🔸 coverage
@[implicit_reducible]
instance NNRat.instSemifield :
Semifield ℚ≥0