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

instance Rat.instField :

Equations

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

theorem Rat.inv_nonneg {a : ℚ} (ha : 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 :

Equations

instance NNRat.instDiv :

Equations

instance NNRat.instZPow :

Pow ℚ≥0 ℤ

Equations

@[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