mathlib documentation

data.rat.basic

Basics for the Rational Numbers

Summary

We define a rational number q as a structure { num, denom, pos, cop }, where

num is the numerator of q,
denom is the denominator of q,
pos is a proof that denom > 0, and
cop is a proof num and denom are coprime.

We then define the expected (discrete) field structure on ℚ and prove basic lemmas about it. Moreoever, we provide the expected casts from ℕ and ℤ into ℚ, i.e. (↑n : ℚ) = n / 1.

Main Definitions

rat is the structure encoding ℚ.
rat.mk n d constructs a rational number q = n / d from n d : ℤ.

Notations

/. is infix notation for rat.mk.

Tags

rat, rationals, field, ℚ, numerator, denominator, num, denom

structure rat :

Type

num : ℤ
denom : ℕ
pos : 0 < c.denom
cop : c.num.nat_abs.coprime c.denom

rat, or ℚ, is the type of rational numbers. It is defined as the set of pairs ⟨n, d⟩ of integers such that d is positive and n and d are coprime. This representation is preferred to the quotient because without periodic reduction, the numerator and denominator can grow exponentially (for example, adding 1/2 to itself repeatedly).

def rat.repr (a : ℚ) :

Equations

{num := n, denom := d, pos := _x, cop := _x_1}.repr = ite (d = 1) (repr n) (repr n ++ "/" ++ repr d)

@[instance]

def rat.has_repr :

Equations

rat.has_repr = {repr := rat.repr}

@[instance]

def rat.has_to_string :

has_to_string ℚ

Equations

rat.has_to_string = {to_string := rat.repr}

@[instance]

meta def rat.has_to_format :

has_to_format ℚ

@[instance]

def rat.encodable :

Equations

rat.encodable = encodable.of_equiv (Σ (n : ℤ), {d // 0 < d ∧ n.nat_abs.coprime d}) {to_fun := λ (_x : ℚ), rat.encodable._match_1 _x, inv_fun := λ (_x : Σ (n : ℤ), {d // 0 < d ∧ n.nat_abs.coprime d}), rat.encodable._match_2 _x, left_inv := rat.encodable._proof_1, right_inv := rat.encodable._proof_2}
rat.encodable._match_1 {num := a, denom := b, pos := c, cop := d} = ⟨a, ⟨b, _⟩⟩
rat.encodable._match_2 ⟨a, ⟨b, _⟩⟩ = {num := a, denom := b, pos := c, cop := d}

def rat.of_int (n : ℤ) :

Embed an integer as a rational number

Equations

rat.of_int n = {num := n, denom := 1, pos := nat.one_pos, cop := _}

@[instance]

def rat.has_zero :

Equations

rat.has_zero = {zero := rat.of_int 0}

@[instance]

def rat.has_one :

Equations

rat.has_one = {one := rat.of_int 1}

@[instance]

def rat.inhabited :

Equations

rat.inhabited = {default := 0}

def rat.mk_pnat (n : ℤ) (a : ℕ+) :

Form the quotient n / d where n:ℤ and d:ℕ+ (not necessarily coprime)

Equations

rat.mk_pnat n ⟨d, dpos⟩ = let n' : ℕ := n.nat_abs, g : ℕ := n'.gcd d in {num := n / ↑g, denom := d / g, pos := _, cop := _}

def rat.mk_nat (n : ℤ) (d : ℕ) :

Form the quotient n / d where n:ℤ and d:ℕ. In the case d = 0, we define n / 0 = 0 by convention.

Equations

rat.mk_nat n d = dite (d = 0) (λ (d0 : d = 0), 0) (λ (d0 : ¬d = 0), rat.mk_pnat n ⟨d, _⟩)

def rat.mk (a a_1 : ℤ) :

Form the quotient n / d where n d : ℤ.

Equations

n /. -[1+ d] = rat.mk_pnat (-n) d.succ_pnat
n /. ↑d = rat.mk_nat n d

theorem rat.mk_pnat_eq (n : ℤ) (d : ℕ) (h : 0 < d) :

rat.mk_pnat n ⟨d, h⟩ = n /. ↑d

theorem rat.mk_nat_eq (n : ℤ) (d : ℕ) :

rat.mk_nat n d = n /. ↑d

@[simp]

theorem rat.mk_zero (n : ℤ) :

n /. 0 = 0

@[simp]

theorem rat.zero_mk_pnat (n : ℕ+) :

rat.mk_pnat 0 n = 0

@[simp]

theorem rat.zero_mk_nat (n : ℕ) :

rat.mk_nat 0 n = 0

@[simp]

theorem rat.zero_mk (n : ℤ) :

0 /. n = 0

@[simp]

theorem rat.mk_eq_zero {a b : ℤ} (b0 : b ≠ 0) :

a /. b = 0 ↔ a = 0

theorem rat.mk_eq {a b c d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0) :

a /. b = c /. d ↔ a * d = c * b

@[simp]

theorem rat.div_mk_div_cancel_left {a b c : ℤ} (c0 : c ≠ 0) :

a * c /. b * c = a /. b

@[simp]

theorem rat.num_denom {a : ℚ} :

a.num /. ↑(a.denom) = a

theorem rat.num_denom' {n : ℤ} {d : ℕ} {h : 0 < d} {c : n.nat_abs.coprime d} :

{num := n, denom := d, pos := h, cop := c} = n /. ↑d

theorem rat.of_int_eq_mk (z : ℤ) :

rat.of_int z = z /. 1

def rat.num_denom_cases_on {C : ℚ → Sort u} (a : ℚ) (H : Π (n : ℤ) (d : ℕ), 0 < d → n.nat_abs.coprime d → C (n /. ↑d)) :

C a

Equations

{num := n, denom := d, pos := h, cop := c}.num_denom_cases_on H = _.mpr (H n d h c)

def rat.num_denom_cases_on' {C : ℚ → Sort u} (a : ℚ) (H : Π (n : ℤ) (d : ℕ), d ≠ 0 → C (n /. ↑d)) :

C a

Equations

a.num_denom_cases_on' H = a.num_denom_cases_on (λ (n : ℤ) (d : ℕ) (h : 0 < d) (c : n.nat_abs.coprime d), H n d _)

theorem rat.num_dvd (a : ℤ) {b : ℤ} (b0 : b ≠ 0) :

(a /. b).num ∣ a

theorem rat.denom_dvd (a b : ℤ) :

↑((a /. b).denom) ∣ b

def rat.add (a a_1 : ℚ) :

Equations

{num := n₁, denom := d₁, pos := h₁, cop := c₁}.add {num := n₂, denom := d₂, pos := h₂, cop := c₂} = rat.mk_pnat (n₁ * ↑d₂ + n₂ * ↑d₁) ⟨d₁ * d₂, _⟩

@[instance]

def rat.has_add :

Equations

rat.has_add = {add := rat.add}

theorem rat.lift_binop_eq (f : ℚ → ℚ → ℚ) (f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ) (fv : ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : 0 < d₁} {c₁ : n₁.nat_abs.coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : 0 < d₂} {c₂ : n₂.nat_abs.coprime d₂}, f {num := n₁, denom := d₁, pos := h₁, cop := c₁} {num := n₂, denom := d₂, pos := h₂, cop := c₂} = f₁ n₁ ↑d₁ n₂ ↑d₂ /. f₂ n₁ ↑d₁ n₂ ↑d₂) (f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0) (a b c d : ℤ) (b0 : b ≠ 0) (d0 : d ≠ 0) (H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → (f₁ n₁ d₁ n₂ d₂) * f₂ a b c d = (f₁ a b c d) * f₂ n₁ d₁ n₂ d₂) :

f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d

@[simp]

theorem rat.add_def {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) :

a /. b + c /. d = (a * d + c * b) /. b * d

def rat.neg (a : ℚ) :

Equations

{num := n, denom := d, pos := h, cop := c}.neg = {num := -n, denom := d, pos := h, cop := _}

@[instance]

def rat.has_neg :

Equations

rat.has_neg = {neg := rat.neg}

@[simp]

theorem rat.neg_def {a b : ℤ} :

-(a /. b) = -a /. b

def rat.mul (a a_1 : ℚ) :

Equations

{num := n₁, denom := d₁, pos := h₁, cop := c₁}.mul {num := n₂, denom := d₂, pos := h₂, cop := c₂} = rat.mk_pnat (n₁ * n₂) ⟨d₁ * d₂, _⟩

@[instance]

def rat.has_mul :

Equations

rat.has_mul = {mul := rat.mul}

@[simp]

theorem rat.mul_def {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) :

(a /. b) * (c /. d) = a * c /. b * d

def rat.inv (a : ℚ) :

Equations

{num := -[1+ n], denom := d, pos := h, cop := c}.inv = {num := -↑d, denom := n + 1, pos := _, cop := _}
{num := ↑(n + 1), denom := d, pos := h, cop := c}.inv = {num := ↑d, denom := n + 1, pos := _, cop := _}
{num := 0, denom := d, pos := h, cop := c}.inv = 0

@[instance]

def rat.has_inv :

Equations

rat.has_inv = {inv := rat.inv}

@[simp]

theorem rat.inv_def {a b : ℤ} :

(a /. b)⁻¹ = b /. a

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.add_left_neg (a : ℚ) :

-a + a = 0

theorem rat.mul_one (a : ℚ) :

a * 1 = a

theorem rat.one_mul (a : ℚ) :

1 * a = a

theorem rat.mul_comm (a b : ℚ) :

a * b = b * a

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.zero_ne_one :

0 ≠ 1

theorem rat.mul_inv_cancel (a : ℚ) (a_1 : a ≠ 0) :

a * a⁻¹ = 1

theorem rat.inv_mul_cancel (a : ℚ) (h : a ≠ 0) :

a⁻¹ * a = 1

@[instance]

def rat.decidable_eq :

decidable_eq ℚ

Equations

rat.decidable_eq = id (λ (_v : ℚ), _v.cases_on (λ (num : ℤ) (denom : ℕ) (pos : 0 < denom) (cop : num.nat_abs.coprime denom) (w : ℚ), w.cases_on (λ (w_num : ℤ) (w_denom : ℕ) (w_pos : 0 < w_denom) (w_cop : w_num.nat_abs.coprime w_denom), decidable.by_cases (λ (a : num = w_num), eq.rec (λ (w_cop : num.nat_abs.coprime w_denom), decidable.by_cases (λ (a : denom = w_denom), eq.rec (λ (w_pos : 0 < denom) (w_cop : num.nat_abs.coprime denom), is_true _) a w_pos w_cop) (λ (a : ¬denom = w_denom), is_false _)) a w_cop) (λ (a : ¬num = w_num), is_false _))))

@[instance]

def rat.field :

Equations

rat.field = {add := rat.add, add_assoc := rat.add_assoc, zero := 0, zero_add := rat.zero_add, add_zero := rat.add_zero, neg := rat.neg, add_left_neg := rat.add_left_neg, add_comm := rat.add_comm, mul := rat.mul, mul_assoc := rat.mul_assoc, one := 1, one_mul := rat.one_mul, mul_one := rat.mul_one, left_distrib := rat.mul_add, right_distrib := rat.add_mul, mul_comm := rat.mul_comm, inv := rat.inv, exists_pair_ne := rat.field._proof_1, mul_inv_cancel := rat.mul_inv_cancel, inv_zero := rat.field._proof_2}

@[instance]

def rat.division_ring :

division_ring ℚ

Equations

rat.division_ring = field.to_division_ring

@[instance]

def rat.integral_domain :

integral_domain ℚ

Equations

rat.integral_domain = field.to_integral_domain

@[instance]

def rat.nontrivial :

@[instance]

def rat.comm_ring :

Equations

rat.comm_ring = euclidean_domain.to_comm_ring ℚ

@[instance]

def rat.comm_semiring :

comm_semiring ℚ

Equations

rat.comm_semiring = comm_ring.to_comm_semiring

@[instance]

def rat.semiring :

Equations

rat.semiring = ring.to_semiring

@[instance]

def rat.add_comm_group :

add_comm_group ℚ

Equations

rat.add_comm_group = ring.to_add_comm_group ℚ

@[instance]

def rat.add_group :

Equations

rat.add_group = add_comm_group.to_add_group ℚ

@[instance]

def rat.add_comm_monoid :

add_comm_monoid ℚ

Equations

rat.add_comm_monoid = add_comm_group.to_add_comm_monoid ℚ

@[instance]

def rat.add_monoid :

Equations

rat.add_monoid = add_group.to_add_monoid ℚ

@[instance]

def rat.add_left_cancel_semigroup :

add_left_cancel_semigroup ℚ

Equations

rat.add_left_cancel_semigroup = add_group.to_left_cancel_add_semigroup

@[instance]

def rat.add_right_cancel_semigroup :

add_right_cancel_semigroup ℚ

Equations

rat.add_right_cancel_semigroup = add_group.to_right_cancel_add_semigroup

@[instance]

def rat.add_comm_semigroup :

add_comm_semigroup ℚ

Equations

rat.add_comm_semigroup = add_comm_monoid.to_add_comm_semigroup ℚ

@[instance]

def rat.add_semigroup :

add_semigroup ℚ

Equations

rat.add_semigroup = add_monoid.to_add_semigroup ℚ

@[instance]

def rat.comm_monoid :

comm_monoid ℚ

Equations

rat.comm_monoid = comm_semiring.to_comm_monoid ℚ

@[instance]

def rat.monoid :

Equations

rat.monoid = ring.to_monoid ℚ

@[instance]

def rat.comm_semigroup :

comm_semigroup ℚ

Equations

rat.comm_semigroup = comm_ring.to_comm_semigroup ℚ

@[instance]

def rat.semigroup :

Equations

rat.semigroup = monoid.to_semigroup ℚ

theorem rat.sub_def {a b c d : ℤ} (b0 : b ≠ 0) (d0 : d ≠ 0) :

a /. b - c /. d = (a * d - c * b) /. b * d

@[simp]

theorem rat.denom_neg_eq_denom (q : ℚ) :

(-q).denom = q.denom

@[simp]

theorem rat.num_neg_eq_neg_num (q : ℚ) :

(-q).num = -q.num

@[simp]

theorem rat.num_zero :

0.num = 0

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

theorem rat.num_ne_zero_of_ne_zero {q : ℚ} (h : q ≠ 0) :

@[simp]

theorem rat.num_one :

1.num = 1

@[simp]

theorem rat.denom_one :

theorem rat.denom_ne_zero (q : ℚ) :

theorem rat.eq_iff_mul_eq_mul {p q : ℚ} :

p = q ↔ (p.num) * ↑(q.denom) = (q.num) * ↑(p.denom)

theorem rat.mk_num_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) :

n ≠ 0

theorem rat.mk_denom_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) :

d ≠ 0

theorem rat.mk_ne_zero_of_ne_zero {n d : ℤ} (h : n ≠ 0) (hd : d ≠ 0) :

n /. d ≠ 0

theorem rat.mul_num_denom (q r : ℚ) :

q * r = (q.num) * r.num /. ↑(q.denom) * r.denom

theorem rat.div_num_denom (q r : ℚ) :

q / r = (q.num) * ↑(r.denom) /. (↑(q.denom)) * r.num

theorem rat.num_denom_mk {q : ℚ} {n d : ℤ} (hn : n ≠ 0) (hd : d ≠ 0) (qdf : q = n /. d) :

∃ (c : ℤ), n = c * q.num ∧ d = c * ↑(q.denom)

theorem rat.mk_pnat_num (n : ℤ) (d : ℕ+) :

(rat.mk_pnat n d).num = n / ↑(n.nat_abs.gcd ↑d)

theorem rat.mk_pnat_denom (n : ℤ) (d : ℕ+) :

(rat.mk_pnat n d).denom = ↑d / n.nat_abs.gcd ↑d

theorem rat.mul_num (q₁ q₂ : ℚ) :

(q₁ * q₂).num = (q₁.num) * q₂.num / ↑(((q₁.num) * q₂.num).nat_abs.gcd ((q₁.denom) * q₂.denom))

theorem rat.mul_denom (q₁ q₂ : ℚ) :

(q₁ * q₂).denom = (q₁.denom) * q₂.denom / ((q₁.num) * q₂.num).nat_abs.gcd ((q₁.denom) * q₂.denom)

theorem rat.mul_self_num (q : ℚ) :

(q * q).num = (q.num) * q.num

theorem rat.mul_self_denom (q : ℚ) :

(q * q).denom = (q.denom) * q.denom

theorem rat.add_num_denom (q r : ℚ) :

q + r = ((q.num) * ↑(r.denom) + (↑(q.denom)) * r.num) /. (↑(q.denom)) * ↑(r.denom)

theorem rat.coe_int_eq_mk (z : ℤ) :

↑z = z /. 1

theorem rat.mk_eq_div (n d : ℤ) :

n /. d = ↑n / ↑d

theorem rat.coe_int_eq_of_int (z : ℤ) :

↑z = rat.of_int z

@[simp]

theorem rat.coe_int_num (n : ℤ) :

@[simp]

theorem rat.coe_int_denom (n : ℤ) :

theorem rat.coe_int_num_of_denom_eq_one {q : ℚ} (hq : q.denom = 1) :

↑(q.num) = q

@[instance]

def rat.can_lift :

can_lift ℚ ℤ

Equations

rat.can_lift = {coe := coe coe_to_lift, cond := λ (q : ℚ), q.denom = 1, prf := rat.can_lift._proof_1}

theorem rat.coe_nat_eq_mk (n : ℕ) :

↑n = ↑n /. 1

@[simp]

theorem rat.coe_nat_num (n : ℕ) :

↑n.num = ↑n

@[simp]

theorem rat.coe_nat_denom (n : ℕ) :

theorem rat.coe_int_inj (m n : ℤ) :

↑m = ↑n ↔ m = n

theorem rat.inv_def' {q : ℚ} :

q⁻¹ = ↑(q.denom) / ↑(q.num)

@[simp]

theorem rat.mul_denom_eq_num {q : ℚ} :

q * ↑(q.denom) = ↑(q.num)

theorem rat.denom_div_cast_eq_one_iff (m n : ℤ) (hn : n ≠ 0) :

(↑m / ↑n).denom = 1 ↔ n ∣ m

theorem rat.num_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : a.nat_abs.coprime b.nat_abs) :

(↑a / ↑b).num = a

theorem rat.denom_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : a.nat_abs.coprime b.nat_abs) :

↑((↑a / ↑b).denom) = b

theorem rat.div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : a.nat_abs.coprime b.nat_abs) (h2 : c.nat_abs.coprime d.nat_abs) (h : ↑a / ↑b = ↑c / ↑d) :

a = c ∧ b = d

theorem rat.coe_int_div_self (n : ℤ) :

↑(n / n) = ↑n / ↑n

theorem rat.coe_nat_div_self (n : ℕ) :

↑(n / n) = ↑n / ↑n

theorem rat.coe_int_div (a b : ℤ) (h : b ∣ a) :

↑(a / b) = ↑a / ↑b

theorem rat.coe_nat_div (a b : ℕ) (h : b ∣ a) :

↑(a / b) = ↑a / ↑b

theorem rat.forall {p : ℚ → Prop} :

(∀ (r : ℚ), p r) ↔ ∀ (a b : ℤ), p (↑a / ↑b)

theorem rat.exists {p : ℚ → Prop} :

(∃ (r : ℚ), p r) ↔ ∃ (a b : ℤ), p (↑a / ↑b)