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 < self.denom
cop : self.num.nat_abs.coprime self.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).

@[protected]

def rat.repr :

String representation of a rational numbers, used in has_repr, has_to_string, and has_to_format instances.

Equations

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

@[protected, instance]

def rat.has_repr :

Equations

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

@[protected, instance]

def rat.has_to_string :

has_to_string ℚ

Equations

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

@[protected, instance]

meta def rat.has_to_format :

has_to_format ℚ

@[protected, 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 := _}

@[protected, instance]

def rat.has_zero :

Equations

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

@[protected, instance]

def rat.has_one :

Equations

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

@[protected, instance]

def rat.inhabited :

Equations

rat.inhabited = {default := 0}

theorem rat.ext_iff {p q : ℚ} :

p = q ↔ p.num = q.num ∧ p.denom = q.denom

@[ext]

theorem rat.ext {p q : ℚ} (hn : p.num = q.num) (hd : p.denom = q.denom) :

p = q

def rat.mk_pnat (n : ℤ) :

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 :

ℤ → ℤ → ℚ

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

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, 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

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

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

@[protected]

def rat.add :

ℚ → ℚ → ℚ

Addition of rational numbers. Use (+) instead.

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₂, _⟩

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

@[protected]

def rat.neg (r : ℚ) :

Negation of rational numbers. Use -r instead.

Equations

r.neg = {num := -r.num, denom := r.denom, pos := _, cop := _}

@[protected, instance]

def rat.has_neg :

Equations

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

@[simp]

theorem rat.neg_def {a b : ℤ} :

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

@[simp]

theorem rat.mk_neg_denom (n d : ℤ) :

n /. -d = -n /. d

@[protected]

def rat.mul :

ℚ → ℚ → ℚ

Multiplication of rational numbers. Use (*) instead.

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₂, _⟩

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

@[protected]

def rat.inv :

Inverse rational number. Use r⁻¹ instead.

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

@[protected, instance]

def rat.has_inv :

Equations

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

@[simp]

theorem rat.inv_def {a b : ℤ} :

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

@[protected]

theorem rat.add_zero (a : ℚ) :

a + 0 = a

@[protected]

theorem rat.zero_add (a : ℚ) :

0 + a = a

@[protected]

theorem rat.add_comm (a b : ℚ) :

a + b = b + a

@[protected]

theorem rat.add_assoc (a b c : ℚ) :

a + b + c = a + (b + c)

@[protected]

theorem rat.add_left_neg (a : ℚ) :

-a + a = 0

@[simp]

theorem rat.mk_zero_one :

0 /. 1 = 0

@[simp]

theorem rat.mk_one_one :

1 /. 1 = 1

@[simp]

theorem rat.mk_neg_one_one :

(-1) /. 1 = -1

@[protected]

theorem rat.mul_one (a : ℚ) :

a * 1 = a

@[protected]

theorem rat.one_mul (a : ℚ) :

1 * a = a

@[protected]

theorem rat.mul_comm (a b : ℚ) :

a * b = b * a

@[protected]

theorem rat.mul_assoc (a b c : ℚ) :

(a * b) * c = a * b * c

@[protected]

theorem rat.add_mul (a b c : ℚ) :

(a + b) * c = a * c + b * c

@[protected]

theorem rat.mul_add (a b c : ℚ) :

a * (b + c) = a * b + a * c

@[protected]

theorem rat.zero_ne_one :

0 ≠ 1

@[protected]

theorem rat.mul_inv_cancel (a : ℚ) :

a ≠ 0 → a * a⁻¹ = 1

@[protected]

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

a⁻¹ * a = 1

@[protected, 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 (λ (ᾰ : num = w_num), eq.rec (λ (w_cop : num.nat_abs.coprime w_denom), decidable.by_cases (λ (ᾰ : denom = w_denom), eq.rec (λ (w_pos : 0 < denom) (w_cop : num.nat_abs.coprime denom), is_true _) ᾰ w_pos w_cop) (λ (ᾰ : ¬denom = w_denom), is_false _)) ᾰ w_cop) (λ (ᾰ : ¬num = w_num), is_false _))))

@[protected, 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, nsmul := comm_ring.nsmul._default 0 rat.add rat.zero_add rat.add_zero, nsmul_zero' := rat.field._proof_1, nsmul_succ' := rat.field._proof_2, neg := rat.neg, sub := comm_ring.sub._default rat.add rat.add_assoc 0 rat.zero_add rat.add_zero (comm_ring.nsmul._default 0 rat.add rat.zero_add rat.add_zero) rat.field._proof_3 rat.field._proof_4 rat.neg, sub_eq_add_neg := rat.field._proof_5, zsmul := comm_ring.zsmul._default rat.add rat.add_assoc 0 rat.zero_add rat.add_zero (comm_ring.nsmul._default 0 rat.add rat.zero_add rat.add_zero) rat.field._proof_6 rat.field._proof_7 rat.neg, zsmul_zero' := rat.field._proof_8, zsmul_succ' := rat.field._proof_9, zsmul_neg' := rat.field._proof_10, 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, npow := comm_ring.npow._default 1 rat.mul rat.one_mul rat.mul_one, npow_zero' := rat.field._proof_11, npow_succ' := rat.field._proof_12, left_distrib := rat.mul_add, right_distrib := rat.add_mul, mul_comm := rat.mul_comm, inv := rat.inv, div := div_inv_monoid.div._default rat.mul rat.mul_assoc 1 rat.one_mul rat.mul_one (comm_ring.npow._default 1 rat.mul rat.one_mul rat.mul_one) rat.field._proof_13 rat.field._proof_14 rat.inv, div_eq_mul_inv := rat.field._proof_15, zpow := div_inv_monoid.zpow._default rat.mul rat.mul_assoc 1 rat.one_mul rat.mul_one (comm_ring.npow._default 1 rat.mul rat.one_mul rat.mul_one) rat.field._proof_16 rat.field._proof_17 rat.inv, zpow_zero' := rat.field._proof_18, zpow_succ' := rat.field._proof_19, zpow_neg' := rat.field._proof_20, exists_pair_ne := rat.field._proof_21, mul_inv_cancel := rat.mul_inv_cancel, inv_zero := rat.field._proof_22}

@[protected, instance]

def rat.division_ring :

division_ring ℚ

Equations

rat.division_ring = field.to_division_ring

@[protected, instance]

def rat.is_domain :

@[protected, instance]

def rat.nontrivial :

@[protected, instance]

def rat.comm_ring :

Equations

rat.comm_ring = euclidean_domain.to_comm_ring

@[protected, instance]

def rat.comm_semiring :

comm_semiring ℚ

Equations

rat.comm_semiring = comm_ring.to_comm_semiring

@[protected, instance]

def rat.semiring :

Equations

rat.semiring = ring.to_semiring

@[protected, instance]

def rat.add_comm_group :

add_comm_group ℚ

Equations

rat.add_comm_group = ring.to_add_comm_group ℚ

@[protected, instance]

def rat.add_group :

Equations

rat.add_group = add_comm_group.to_add_group ℚ

@[protected, instance]

def rat.add_comm_monoid :

add_comm_monoid ℚ

Equations

rat.add_comm_monoid = add_comm_group.to_add_comm_monoid ℚ

@[protected, instance]

def rat.add_monoid :

Equations

rat.add_monoid = sub_neg_monoid.to_add_monoid ℚ

@[protected, instance]

def rat.add_left_cancel_semigroup :

add_left_cancel_semigroup ℚ

Equations

rat.add_left_cancel_semigroup = add_left_cancel_monoid.to_add_left_cancel_semigroup ℚ

@[protected, instance]

def rat.add_right_cancel_semigroup :

add_right_cancel_semigroup ℚ

Equations

rat.add_right_cancel_semigroup = add_right_cancel_monoid.to_add_right_cancel_semigroup ℚ

@[protected, instance]

def rat.add_comm_semigroup :

add_comm_semigroup ℚ

Equations

rat.add_comm_semigroup = add_comm_monoid.to_add_comm_semigroup ℚ

@[protected, instance]

def rat.add_semigroup :

add_semigroup ℚ

Equations

rat.add_semigroup = add_monoid.to_add_semigroup ℚ

@[protected, instance]

def rat.comm_monoid :

comm_monoid ℚ

Equations

rat.comm_monoid = comm_ring.to_comm_monoid ℚ

@[protected, instance]

def rat.monoid :

Equations

rat.monoid = ring.to_monoid ℚ

@[protected, instance]

def rat.comm_semigroup :

comm_semigroup ℚ

Equations

rat.comm_semigroup = comm_monoid.to_comm_semigroup ℚ

@[protected, instance]

def rat.semigroup :

Equations

rat.semigroup = semigroup_with_zero.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

@[simp]

theorem rat.denom_zero :

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 : ℤ} (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.num_mk (n d : ℤ) :

(n /. d).num = (d.sign) * n / ↑(n.gcd d)

theorem rat.denom_mk (n d : ℤ) :

(n /. d).denom = ite (d = 0) 1 (d.nat_abs / n.gcd d)

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

(rat.mk_pnat n d).denom ∣ d.val

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

(q₁ + q₂).denom ∣ (q₁.denom) * q₂.denom

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

(q₁ * q₂).denom ∣ (q₁.denom) * q₂.denom

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)

@[protected]

theorem rat.add_mk (a b c : ℤ) :

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

theorem rat.coe_int_eq_mk (z : ℤ) :

↑z = z /. 1

theorem rat.mk_eq_div (n d : ℤ) :

n /. d = ↑n / ↑d

@[simp]

theorem rat.num_div_denom (r : ℚ) :

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

theorem rat.exists_eq_mul_div_num_and_eq_mul_div_denom (n : ℤ) {d : ℤ} (d_ne_zero : d ≠ 0) :

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

theorem rat.coe_int_eq_of_int (z : ℤ) :

↑z = rat.of_int z

@[simp, norm_cast]

theorem rat.coe_int_num (n : ℤ) :

@[simp, norm_cast]

theorem rat.coe_int_denom (n : ℤ) :

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

↑(q.num) = q

theorem rat.denom_eq_one_iff (r : ℚ) :

r.denom = 1 ↔ ↑(r.num) = r

@[protected, instance]

def rat.int.can_lift :

can_lift ℚ ℤ

Equations

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

theorem rat.coe_nat_eq_mk (n : ℕ) :

↑n = ↑n /. 1

@[simp, norm_cast]

theorem rat.coe_nat_num (n : ℕ) :

↑n.num = ↑n

@[simp, norm_cast]

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

@[norm_cast]

theorem rat.coe_int_div_self (n : ℤ) :

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

@[norm_cast]

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.inv_coe_int_num {a : ℤ} (ha0 : 0 < a) :

(↑a)⁻¹.num = 1

theorem rat.inv_coe_nat_num {a : ℕ} (ha0 : 0 < a) :

(↑a)⁻¹.num = 1

theorem rat.inv_coe_int_denom {a : ℤ} (ha0 : 0 < a) :

↑((↑a)⁻¹.denom) = a

theorem rat.inv_coe_nat_denom {a : ℕ} (ha0 : 0 < a) :

(↑a)⁻¹.denom = a

@[protected]

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

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

@[protected]

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

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