# Basics for the Rational Numbers #

## Summary #

We define the integral domain structure on ℚ and prove basic lemmas about it. The definition of the field structure on ℚ will be done in Mathlib.Data.Rat.Basic once the Field class has been defined.

## Main Definitions #

• Rat.divInt n d constructs a rational number q = n / d from n d : ℤ.

## Notations #

• /. is infix notation for Rat.divInt.
theorem Rat.pos (a : ) :
0 < a.den
theorem Rat.mk'_num_den (q : ) :
{ num := q.num, den := q.den, den_nz := , reduced := } = q
@[simp]
theorem Rat.ofInt_eq_cast (n : ) :
= n
@[simp]
theorem Rat.num_ofNat (n : ) :
(OfNat.ofNat n).num =
@[simp]
theorem Rat.den_ofNat (n : ) :
(OfNat.ofNat n).den = 1
@[simp]
theorem Rat.num_natCast (n : ) :
(↑n).num = n
@[simp]
theorem Rat.den_natCast (n : ) :
(↑n).den = 1
@[simp]
theorem Rat.num_intCast (n : ) :
(↑n).num = n
@[simp]
theorem Rat.den_intCast (n : ) :
(↑n).den = 1
@[deprecated Rat.num_intCast]
theorem Rat.coe_int_num (n : ) :
(↑n).num = n

Alias of Rat.num_intCast.

@[deprecated Rat.den_intCast]
theorem Rat.coe_int_den (n : ) :
(↑n).den = 1

Alias of Rat.den_intCast.

@[simp]
theorem Rat.natCast_inj {m : } {n : } :
m = n m = n
@[simp]
theorem Rat.intCast_eq_zero {n : } :
n = 0 n = 0
@[simp]
theorem Rat.natCast_eq_zero {n : } :
n = 0 n = 0
@[simp]
theorem Rat.intCast_eq_one {n : } :
n = 1 n = 1
@[simp]
theorem Rat.natCast_eq_one {n : } :
n = 1 n = 1
theorem Rat.mkRat_eq_divInt (n : ) (d : ) :
mkRat n d = Rat.divInt n d
@[simp]
theorem Rat.mk'_zero (d : ) (h : d 0) (w : (Int.natAbs 0).Coprime d) :
{ num := 0, den := d, den_nz := h, reduced := w } = 0
@[simp]
theorem Rat.num_eq_zero {q : } :
q.num = 0 q = 0
theorem Rat.num_ne_zero {q : } :
q.num 0 q 0
@[simp]
theorem Rat.den_ne_zero (q : ) :
q.den 0
@[simp]
theorem Rat.num_nonneg {q : } :
0 q.num 0 q
@[simp]
theorem Rat.divInt_eq_zero {a : } {b : } (b0 : b 0) :
= 0 a = 0
theorem Rat.divInt_ne_zero {a : } {b : } (b0 : b 0) :
0 a 0
theorem Rat.normalize_eq_mk' (n : ) (d : ) (h : d 0) (c : n.natAbs.gcd d = 1) :
= { num := n, den := d, den_nz := h, reduced := c }
@[simp]
theorem Rat.mkRat_num_den' (a : ) :
mkRat a.num a.den = a

Alias of Rat.mkRat_self.

theorem Rat.num_divInt_den (q : ) :
Rat.divInt q.num q.den = q
theorem Rat.mk'_eq_divInt {n : } {d : } {h : d 0} {c : n.natAbs.Coprime d} :
{ num := n, den := d, den_nz := h, reduced := c } = Rat.divInt n d
theorem Rat.intCast_eq_divInt (z : ) :
z =
@[simp]
theorem Rat.divInt_self' {n : } (hn : n 0) :
= 1
def Rat.numDenCasesOn {C : Sort u} (a : ) :
((n : ) → (d : ) → 0 < dn.natAbs.Coprime dC (Rat.divInt n d))C a

Define a (dependent) function or prove ∀ r : ℚ, p r by dealing with rational numbers of the form n /. d with 0 < d and coprime n, d.

Equations
• { num := n, den := d, den_nz := h, reduced := c }.numDenCasesOn x = .mpr (x n d c)
Instances For
def Rat.numDenCasesOn' {C : Sort u} (a : ) (H : (n : ) → (d : ) → d 0C (Rat.divInt n d)) :
C a

Define a (dependent) function or prove ∀ r : ℚ, p r by dealing with rational numbers of the form n /. d with d ≠ 0.

Equations
• a.numDenCasesOn' H = a.numDenCasesOn fun (n : ) (d : ) (h : 0 < d) (x : n.natAbs.Coprime d) => H n d
Instances For
def Rat.numDenCasesOn'' {C : Sort u} (a : ) (H : (n : ) → (d : ) → (nz : d 0) → (red : n.natAbs.Coprime d) → C { num := n, den := d, den_nz := nz, reduced := red }) :
C a

Define a (dependent) function or prove ∀ r : ℚ, p r by dealing with rational numbers of the form mk' n d with d ≠ 0.

Equations
• a.numDenCasesOn'' H = a.numDenCasesOn fun (n : ) (d : ) (h : 0 < d) (h' : n.natAbs.Coprime d) => .mpr (H n d h')
Instances For
theorem Rat.lift_binop_eq (f : ) (f₁ : ) (f₂ : ) (fv : ∀ {n₁ : } {d₁ : } {h₁ : d₁ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : } {d₂ : } {h₂ : d₂ 0} {c₂ : n₂.natAbs.Coprime d₂}, f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = Rat.divInt (f₁ n₁ (↑d₁) n₂ d₂) (f₂ n₁ (↑d₁) n₂ d₂)) (f0 : ∀ {n₁ d₁ n₂ d₂ : }, d₁ 0d₂ 0f₂ n₁ d₁ n₂ d₂ 0) (a : ) (b : ) (c : ) (d : ) (b0 : b 0) (d0 : d 0) (H : ∀ {n₁ d₁ n₂ d₂ : }, a * d₁ = n₁ * bc * d₂ = n₂ * df₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂) :
f (Rat.divInt a b) (Rat.divInt c d) = Rat.divInt (f₁ a b c d) (f₂ a b c d)
theorem Rat.add_def'' {a : } {b : } {c : } {d : } (b0 : b 0) (d0 : d 0) :
+ = Rat.divInt (a * d + c * b) (b * d)
theorem Rat.neg_def (q : ) :
-q = Rat.divInt (-q.num) q.den
@[simp]
theorem Rat.divInt_neg (n : ) (d : ) :
@[deprecated Rat.divInt_neg]
theorem Rat.divInt_neg_den (n : ) (d : ) :

Alias of Rat.divInt_neg.

@[deprecated Rat.divInt_sub_divInt]
theorem Rat.sub_def'' {a : } {b : } {c : } {d : } (b0 : b 0) (d0 : d 0) :
- = Rat.divInt (a * d - c * b) (b * d)
@[simp]
theorem Rat.divInt_mul_divInt' (n₁ : ) (d₁ : ) (n₂ : ) (d₂ : ) :
Rat.divInt n₁ d₁ * Rat.divInt n₂ d₂ = Rat.divInt (n₁ * n₂) (d₁ * d₂)
theorem Rat.mk'_mul_mk' (n₁ : ) (n₂ : ) (d₁ : ) (d₂ : ) (hd₁ : d₁ 0) (hd₂ : d₂ 0) (hnd₁ : n₁.natAbs.Coprime d₁) (hnd₂ : n₂.natAbs.Coprime d₂) (h₁₂ : n₁.natAbs.Coprime d₂) (h₂₁ : n₂.natAbs.Coprime d₁) :
{ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ } * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ } = { num := n₁ * n₂, den := d₁ * d₂, den_nz := , reduced := }
theorem Rat.mul_eq_mkRat (q : ) (r : ) :
q * r = mkRat (q.num * r.num) (q.den * r.den)
theorem Rat.divInt_eq_divInt {d₁ : } {d₂ : } {n₁ : } {n₂ : } (z₁ : d₁ 0) (z₂ : d₂ 0) :
Rat.divInt n₁ d₁ = Rat.divInt n₂ d₂ n₁ * d₂ = n₂ * d₁

Alias of Rat.divInt_eq_iff.

@[deprecated Rat.mul_eq_mkRat]
theorem Rat.mul_num_den (q : ) (r : ) :
q * r = mkRat (q.num * r.num) (q.den * r.den)

Alias of Rat.mul_eq_mkRat.

instance Rat.instPowNat :
Equations
• Rat.instPowNat = { pow := fun (q : ) (n : ) => { num := q.num ^ n, den := q.den ^ n, den_nz := , reduced := } }
theorem Rat.pow_def (q : ) (n : ) :
q ^ n = { num := q.num ^ n, den := q.den ^ n, den_nz := , reduced := }
theorem Rat.pow_eq_mkRat (q : ) (n : ) :
q ^ n = mkRat (q.num ^ n) (q.den ^ n)
theorem Rat.pow_eq_divInt (q : ) (n : ) :
q ^ n = Rat.divInt (q.num ^ n) (q.den ^ n)
@[simp]
theorem Rat.num_pow (q : ) (n : ) :
(q ^ n).num = q.num ^ n
@[simp]
theorem Rat.den_pow (q : ) (n : ) :
(q ^ n).den = q.den ^ n
@[simp]
theorem Rat.mk'_pow (num : ) (den : ) (hd : den 0) (hdn : num.natAbs.Coprime den) (n : ) :
{ num := num, den := den, den_nz := hd, reduced := hdn } ^ n = { num := num ^ n, den := den ^ n, den_nz := , reduced := }
instance Rat.instInv :
Equations
@[simp]
theorem Rat.inv_divInt' (a : ) (b : ) :
@[simp]
theorem Rat.inv_mkRat (a : ) (b : ) :
(mkRat a b)⁻¹ = Rat.divInt (↑b) a
theorem Rat.inv_def' (q : ) :
q⁻¹ = Rat.divInt (↑q.den) q.num
@[simp]
theorem Rat.divInt_div_divInt (n₁ : ) (d₁ : ) (n₂ : ) (d₂ : ) :
Rat.divInt n₁ d₁ / Rat.divInt n₂ d₂ = Rat.divInt (n₁ * d₂) (d₁ * n₂)
theorem Rat.div_def' (q : ) (r : ) :
q / r = Rat.divInt (q.num * r.den) (q.den * r.num)
@[deprecated Rat.div_def']
theorem Rat.div_num_den (q : ) (r : ) :
q / r = Rat.divInt (q.num * r.den) (q.den * r.num)

Alias of Rat.div_def'.

theorem Rat.add_zero (a : ) :
a + 0 = a
theorem Rat.zero_add (a : ) :
0 + a = a
theorem Rat.add_comm (a : ) (b : ) :
a + b = b + a
theorem Rat.add_assoc (a : ) (b : ) (c : ) :
a + b + c = a + (b + c)
theorem Rat.neg_add_cancel (a : ) :
-a + a = 0
@[deprecated Rat.zero_divInt]
@[simp]
theorem Rat.divInt_one (n : ) :
= n
@[simp]
theorem Rat.mkRat_one (n : ) :
mkRat n 1 = n
@[deprecated Rat.divInt_one]
theorem Rat.mul_assoc (a : ) (b : ) (c : ) :
a * b * c = a * (b * c)
theorem Rat.add_mul (a : ) (b : ) (c : ) :
(a + b) * c = a * c + b * c
theorem Rat.mul_add (a : ) (b : ) (c : ) :
a * (b + c) = a * b + a * c
theorem Rat.mul_inv_cancel (a : ) :
a 0a * a⁻¹ = 1
theorem Rat.inv_mul_cancel (a : ) (h : a 0) :
a⁻¹ * a = 1
instance Rat.nontrivial :
Equations

### The rational numbers are a group #

Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
instance Rat.commMonoid :
Equations
instance Rat.monoid :
Equations
Equations
instance Rat.semigroup :
Equations
theorem Rat.eq_iff_mul_eq_mul {p : } {q : } :
p = q p.num * q.den = q.num * p.den
@[simp]
theorem Rat.den_neg_eq_den (q : ) :
(-q).den = q.den
@[simp]
theorem Rat.num_neg_eq_neg_num (q : ) :
(-q).num = -q.num
@[simp]
theorem Rat.num_zero :
= 0
@[simp]
theorem Rat.den_zero :
= 1
theorem Rat.zero_of_num_zero {q : } (hq : q.num = 0) :
q = 0
theorem Rat.zero_iff_num_zero {q : } :
q = 0 q.num = 0
@[simp]
theorem Rat.num_one :
= 1
@[simp]
theorem Rat.den_one :
= 1
theorem Rat.mk_num_ne_zero_of_ne_zero {q : } {n : } {d : } (hq : q 0) (hqnd : q = ) :
n 0
theorem Rat.mk_denom_ne_zero_of_ne_zero {q : } {n : } {d : } (hq : q 0) (hqnd : q = ) :
d 0
theorem Rat.divInt_ne_zero_of_ne_zero {n : } {d : } (h : n 0) (hd : d 0) :
0
theorem Rat.nonneg_antisymm {q : } :
0 q0 -qq = 0
theorem Rat.nonneg_total (a : ) :
0 a 0 -a
theorem Rat.add_divInt (a : ) (b : ) (c : ) :
Rat.divInt (a + b) c = +
theorem Rat.divInt_eq_div (n : ) (d : ) :
= n / d
theorem Rat.intCast_div_eq_divInt (n : ) (d : ) :
n / d =
theorem Rat.natCast_div_eq_divInt (n : ) (d : ) :
n / d = Rat.divInt n d
theorem Rat.divInt_mul_divInt_cancel {x : } (hx : x 0) (n : ) (d : ) :
* =
theorem Rat.coe_int_num_of_den_eq_one {q : } (hq : q.den = 1) :
q.num = q
theorem Rat.eq_num_of_isInt {q : } (h : q.isInt = true) :
q = q.num
theorem Rat.den_eq_one_iff (r : ) :
r.den = 1 r.num = r
instance Rat.canLift :
CanLift Int.cast fun (q : ) => q.den = 1
Equations
@[deprecated Rat.intCast_eq_divInt]
theorem Rat.coe_int_eq_divInt (z : ) :
z =

Alias of Rat.intCast_eq_divInt.

@[deprecated Rat.intCast_div_eq_divInt]
theorem Rat.coe_int_div_eq_divInt (n : ) (d : ) :
n / d =

Alias of Rat.intCast_div_eq_divInt.

theorem Rat.coe_int_inj (m : ) (n : ) :
m = n m = n