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

instance Rat.instField : Field ℚ

Equations

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

Extra instances to short-circuit type class resolution

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

instance Rat.instDivisionRing : DivisionRing ℚ

Equations

• Rat.instDivisionRing = inferInstance

theorem Rat.inv_nonneg {a : ℚ} (ha : 0 ≤ a) : 0 ≤ a⁻¹

theorem Rat.div_nonneg {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b

theorem Rat.zpow_nonneg {a : ℚ} (ha : 0 ≤ a) (n : ℤ) : 0 ≤ a ^ n

instance NNRat.instInv : Inv ℚ≥0

Equations

• NNRat.instInv = { inv := fun (x : ℚ≥0) => ⟨(↑x)⁻¹, ⋯⟩ }

instance NNRat.instDiv : Div ℚ≥0

Equations

• NNRat.instDiv = { div := fun (x y : ℚ≥0) => ⟨↑x / ↑y, ⋯⟩ }

instance NNRat.instZPow : Pow ℚ≥0 ℤ

Equations

• NNRat.instZPow = { pow := fun (x : ℚ≥0) (n : ℤ) => ⟨↑x ^ n, ⋯⟩ }

@[simp]

theorem NNRat.coe_inv (q : ℚ≥0) : ↑q⁻¹ = (↑q)⁻¹

@[simp]

theorem NNRat.coe_div (p q : ℚ≥0) : ↑(p / q) = ↑p / ↑q

@[simp]

theorem NNRat.coe_zpow (p : ℚ≥0) (n : ℤ) : ↑(p ^ n) = ↑p ^ n

theorem NNRat.inv_def (q : ℚ≥0) : q⁻¹ = divNat q.den q.num

theorem NNRat.div_def (p q : ℚ≥0) : p / q = divNat (p.num * q.den) (p.den * q.num)

theorem NNRat.num_inv_of_ne_zero {q : ℚ≥0} (hq : q ≠ 0) : q⁻¹.num = q.den

theorem NNRat.den_inv_of_ne_zero {q : ℚ≥0} (hq : q ≠ 0) : q⁻¹.den = q.num

@[simp]

theorem NNRat.num_div_den (q : ℚ≥0) : ↑q.num / ↑q.den = q

instance NNRat.instSemifield : Semifield ℚ≥0

Equations

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