mathlib documentation

data.rat.defs

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 integral domain structure on ℚ and prove basic lemmas about it. The definition of the field structure on ℚ will be done in data.rat.basic once the field class has been defined.

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).

Instances for rat

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

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

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

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

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

rat.mk_nat n d = rat.mk n ↑d

@[simp]

theorem rat.mk_zero (n : ℤ) :

rat.mk 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 : ℤ) :

rat.mk 0 n = 0

@[simp]

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

rat.mk a b = 0 ↔ a = 0

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

rat.mk a b ≠ 0 ↔ a ≠ 0

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

rat.mk a b = rat.mk c d ↔ a * d = c * b

@[simp]

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

rat.mk (a * c) (b * c) = rat.mk a b

@[simp]

theorem rat.num_denom {a : ℚ} :

rat.mk 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} = rat.mk n ↑d

theorem rat.of_int_eq_mk (z : ℤ) :

rat.of_int z = rat.mk z 1

def rat.num_denom_cases_on {C : ℚ → Sort u} (a : ℚ) (H : Π (n : ℤ) (d : ℕ), 0 < d → n.nat_abs.coprime d → C (rat.mk 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 (rat.mk 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) :

(rat.mk a b).num ∣ a

theorem rat.denom_dvd (a b : ℤ) :

↑((rat.mk 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₂} = rat.mk (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 (rat.mk a b) (rat.mk c d) = rat.mk (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) :

rat.mk a b + rat.mk c d = rat.mk (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 : ℤ} :

-rat.mk a b = rat.mk (-a) b

@[simp]

theorem rat.mk_neg_denom (n d : ℤ) :

rat.mk n (-d) = rat.mk (-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) :

rat.mk a b * rat.mk c d = rat.mk (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}

@[protected, instance]

def rat.has_div :

Equations

rat.has_div = {div := λ (a b : ℚ), a * b⁻¹}

@[simp]

theorem rat.inv_def {a b : ℤ} :

(rat.mk a b)⁻¹ = rat.mk 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 :

rat.mk 0 1 = 0

@[simp]

theorem rat.mk_one_one :

rat.mk 1 1 = 1

@[simp]

theorem rat.mk_neg_one_one :

rat.mk (-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), decidable.is_true _) ᾰ w_pos w_cop) (λ (ᾰ : ¬denom = w_denom), decidable.is_false _)) ᾰ w_cop) (λ (ᾰ : ¬num = w_num), decidable.is_false _))))

At this point in the import hierarchy we have not defined the field typeclass. Instead we'll instantiate comm_ring and comm_group_with_zero at this point. The rat.field instance and any field-specific lemmas can be found in data.rat.basic.

@[protected, instance]

def rat.comm_ring :

Equations

rat.comm_ring = {add := has_add.add rat.has_add, add_assoc := rat.add_assoc, zero := 0, zero_add := rat.zero_add, add_zero := rat.add_zero, nsmul := ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero, nsmul_zero' := rat.comm_ring._proof_1, nsmul_succ' := rat.comm_ring._proof_2, neg := has_neg.neg rat.has_neg, sub := ring.sub._default has_add.add rat.add_assoc 0 rat.zero_add rat.add_zero (ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero) rat.comm_ring._proof_3 rat.comm_ring._proof_4 has_neg.neg, sub_eq_add_neg := rat.comm_ring._proof_5, zsmul := ring.zsmul._default has_add.add rat.add_assoc 0 rat.zero_add rat.add_zero (ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero) rat.comm_ring._proof_6 rat.comm_ring._proof_7 has_neg.neg, zsmul_zero' := rat.comm_ring._proof_8, zsmul_succ' := rat.comm_ring._proof_9, zsmul_neg' := rat.comm_ring._proof_10, add_left_neg := rat.add_left_neg, add_comm := rat.add_comm, int_cast := ring.int_cast._default (λ (n : ℕ), rat.of_int ↑n) has_add.add rat.add_assoc 0 rat.zero_add rat.add_zero (ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero) rat.comm_ring._proof_11 rat.comm_ring._proof_12 1 rat.comm_ring._proof_13 rat.comm_ring._proof_14 has_neg.neg (ring.sub._default has_add.add rat.add_assoc 0 rat.zero_add rat.add_zero (ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero) rat.comm_ring._proof_3 rat.comm_ring._proof_4 has_neg.neg) rat.comm_ring._proof_15 (ring.zsmul._default has_add.add rat.add_assoc 0 rat.zero_add rat.add_zero (ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero) rat.comm_ring._proof_6 rat.comm_ring._proof_7 has_neg.neg) rat.comm_ring._proof_16 rat.comm_ring._proof_17 rat.comm_ring._proof_18 rat.add_left_neg, nat_cast := λ (n : ℕ), rat.of_int ↑n, one := 1, nat_cast_zero := rat.comm_ring._proof_19, nat_cast_succ := rat.comm_ring._proof_20, int_cast_of_nat := rat.comm_ring._proof_21, int_cast_neg_succ_of_nat := rat.comm_ring._proof_22, mul := has_mul.mul rat.has_mul, mul_assoc := rat.mul_assoc, one_mul := rat.one_mul, mul_one := rat.mul_one, npow := ring.npow._default 1 has_mul.mul rat.one_mul rat.mul_one, npow_zero' := rat.comm_ring._proof_23, npow_succ' := rat.comm_ring._proof_24, left_distrib := rat.mul_add, right_distrib := rat.add_mul, mul_comm := rat.mul_comm}

@[protected, instance]

def rat.comm_group_with_zero :

comm_group_with_zero ℚ

Equations

rat.comm_group_with_zero = {mul := has_mul.mul rat.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := comm_ring.npow rat.comm_ring, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := 0, zero_mul := rat.comm_group_with_zero._proof_1, mul_zero := rat.comm_group_with_zero._proof_2, inv := has_inv.inv rat.has_inv, div := has_div.div rat.has_div, div_eq_mul_inv := rat.comm_group_with_zero._proof_3, zpow := group_with_zero.zpow._default has_mul.mul comm_ring.mul_assoc 1 comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' has_inv.inv, zpow_zero' := rat.comm_group_with_zero._proof_4, zpow_succ' := rat.comm_group_with_zero._proof_5, zpow_neg' := rat.comm_group_with_zero._proof_6, exists_pair_ne := rat.comm_group_with_zero._proof_7, inv_zero := rat.comm_group_with_zero._proof_8, mul_inv_cancel := rat.mul_inv_cancel}

@[protected, instance]

def rat.is_domain :

@[protected, instance]

def rat.nontrivial :

@[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 = non_unital_non_assoc_ring.to_add_comm_group ℚ

@[protected, instance]

def rat.add_group :

Equations

rat.add_group = add_group_with_one.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 = add_monoid_with_one.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 = non_unital_comm_ring.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) :

rat.mk a b - rat.mk c d = rat.mk (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 = rat.mk n d) :

n ≠ 0

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

d ≠ 0

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

rat.mk n d ≠ 0

theorem rat.mul_num_denom (q r : ℚ) :

q * r = rat.mk (q.num * r.num) ↑(q.denom * r.denom)

theorem rat.div_num_denom (q r : ℚ) :

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

theorem rat.num_denom_mk {q : ℚ} {n d : ℤ} (hd : d ≠ 0) (qdf : q = rat.mk 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 : ℤ) :

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

theorem rat.denom_mk (n d : ℤ) :

(rat.mk 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 = rat.mk (q.num * ↑(r.denom) + ↑(q.denom) * r.num) (↑(q.denom) * ↑(r.denom))

@[protected]

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

rat.mk (a + b) c = rat.mk a c + rat.mk b c

theorem rat.coe_int_eq_mk (z : ℤ) :

↑z = rat.mk z 1

theorem rat.mk_eq_div (n d : ℤ) :

rat.mk n d = ↑n / ↑d

theorem rat.mk_mul_mk_cancel {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :

rat.mk n x * rat.mk x d = rat.mk n d

theorem rat.mk_div_mk_cancel_left {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :

rat.mk n x / rat.mk d x = rat.mk n d

theorem rat.mk_div_mk_cancel_right {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :

rat.mk x n / rat.mk x d = rat.mk d n

theorem rat.coe_int_div_eq_mk {n d : ℤ} :

↑n / ↑d = rat.mk 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.mul_num_denom' (q r : ℚ) :

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

theorem rat.add_num_denom' (q r : ℚ) :

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

theorem rat.substr_num_denom' (q r : ℚ) :

(q - r).num * ↑(q.denom) * ↑(r.denom) = (q.num * ↑(r.denom) - r.num * ↑(q.denom)) * ↑((q - r).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 = rat.mk ↑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)

Denominator as `ℕ+` #

def rat.pnat_denom (x : ℚ) :

Denominator as ℕ+.

Equations

x.pnat_denom = ⟨x.denom, _⟩

@[simp]

theorem rat.coe_pnat_denom (x : ℚ) :

↑(x.pnat_denom) = x.denom

@[simp]

theorem rat.mk_pnat_pnat_denom_eq (x : ℚ) :

rat.mk_pnat x.num x.pnat_denom = x

theorem rat.pnat_denom_eq_iff_denom_eq {x : ℚ} {n : ℕ+} :

x.pnat_denom = n ↔ x.denom = ↑n

@[simp]

theorem rat.pnat_denom_one :

1.pnat_denom = 1

@[simp]

theorem rat.pnat_denom_zero :

0.pnat_denom = 1