Additional lemmas about the Rational Numbers #

source

theorem Rat.ext {p : Rat} {q : Rat} :

p.num = q.num → p.den = q.den → p = q

source

@[simp]

theorem Rat.mk_den_one {r : Int} :

{ num := r, den := 1, den_nz := Nat.one_ne_zero, reduced := ⋯ } = ↑r

source

@[simp]

theorem Rat.zero_num :

Rat.num 0 = 0

source

@[simp]

theorem Rat.zero_den :

Rat.den 0 = 1

source

@[simp]

theorem Rat.one_num :

Rat.num 1 = 1

source

@[simp]

theorem Rat.one_den :

Rat.den 1 = 1

source

@[simp]

theorem Rat.maybeNormalize_eq {num : Int} {den : Nat} {g : Nat} (den_nz : den / g ≠ 0) (reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)) :

Rat.maybeNormalize num den g den_nz reduced = { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }

source

theorem Rat.normalize.reduced' {num : Int} {den : Nat} {g : Nat} (den_nz : den ≠ 0) (e : g = num.natAbs.gcd den) :

(num / ↑g).natAbs.Coprime (den / g)

source

theorem Rat.normalize_eq {num : Int} {den : Nat} (den_nz : den ≠ 0) :

Rat.normalize num den den_nz = { num := num / ↑(num.natAbs.gcd den), den := den / num.natAbs.gcd den, den_nz := ⋯, reduced := ⋯ }

source

@[simp]

theorem Rat.normalize_zero {d : Nat} (nz : d ≠ 0) :

Rat.normalize 0 d nz = 0

source

theorem Rat.mk_eq_normalize (num : Int) (den : Nat) (nz : den ≠ 0) (c : num.natAbs.Coprime den) :

{ num := num, den := den, den_nz := nz, reduced := c } = Rat.normalize num den nz

source

theorem Rat.normalize_self (r : Rat) :

Rat.normalize r.num r.den ⋯ = r

source

theorem Rat.normalize_mul_left {d : Nat} {n : Int} {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) :

Rat.normalize (↑a * n) (a * d) ⋯ = Rat.normalize n d d0

source

theorem Rat.normalize_mul_right {d : Nat} {n : Int} {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) :

Rat.normalize (n * ↑a) (d * a) ⋯ = Rat.normalize n d d0

source

theorem Rat.normalize_eq_iff {d₁ : Nat} {d₂ : Nat} {n₁ : Int} {n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :

Rat.normalize n₁ d₁ z₁ = Rat.normalize n₂ d₂ z₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁

source

theorem Rat.maybeNormalize_eq_normalize {num : Int} {den : Nat} {g : Nat} (den_nz : den / g ≠ 0) (reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)) (hn : ↑g ∣ num) (hd : g ∣ den) :

Rat.maybeNormalize num den g den_nz reduced = Rat.normalize num den ⋯

source

@[simp]

theorem Rat.normalize_eq_zero {d : Nat} {n : Int} (d0 : d ≠ 0) :

Rat.normalize n d d0 = 0 ↔ n = 0

source

theorem Rat.normalize_num_den' (num : Int) (den : Nat) (nz : den ≠ 0) :

∃ (d : Nat), d ≠ 0 ∧ num = (Rat.normalize num den nz).num * ↑d ∧ den = (Rat.normalize num den nz).den * d

source

theorem Rat.normalize_num_den {n : Int} {d : Nat} {z : d ≠ 0} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'} (h : Rat.normalize n d z = { num := n', den := d', den_nz := z', reduced := c }) :

∃ (m : Nat), m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m

source

theorem Rat.normalize_eq_mkRat {num : Int} {den : Nat} (den_nz : den ≠ 0) :

Rat.normalize num den den_nz = mkRat num den

source

theorem Rat.mkRat_num_den {d : Nat} {n : Int} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'} (z : d ≠ 0) (h : mkRat n d = { num := n', den := d', den_nz := z', reduced := c }) :

∃ (m : Nat), m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m

source

theorem Rat.mkRat_def (n : Int) (d : Nat) :

mkRat n d = if d0 : d = 0 then 0 else Rat.normalize n d d0

source

theorem Rat.mkRat_self (a : Rat) :

mkRat a.num a.den = a

source

theorem Rat.mk_eq_mkRat (num : Int) (den : Nat) (nz : den ≠ 0) (c : num.natAbs.Coprime den) :

{ num := num, den := den, den_nz := nz, reduced := c } = mkRat num den

source

@[simp]

theorem Rat.zero_mkRat (n : Nat) :

mkRat 0 n = 0

source

@[simp]

theorem Rat.mkRat_zero (n : Int) :

mkRat n 0 = 0

source

theorem Rat.mkRat_eq_zero {d : Nat} {n : Int} (d0 : d ≠ 0) :

mkRat n d = 0 ↔ n = 0

source

theorem Rat.mkRat_ne_zero {d : Nat} {n : Int} (d0 : d ≠ 0) :

mkRat n d ≠ 0 ↔ n ≠ 0

source

theorem Rat.mkRat_mul_left {n : Int} {d : Nat} {a : Nat} (a0 : a ≠ 0) :

mkRat (↑a * n) (a * d) = mkRat n d

source

theorem Rat.mkRat_mul_right {n : Int} {d : Nat} {a : Nat} (a0 : a ≠ 0) :

mkRat (n * ↑a) (d * a) = mkRat n d

source

theorem Rat.mkRat_eq_iff {d₁ : Nat} {d₂ : Nat} {n₁ : Int} {n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :

mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁

source

@[simp]

theorem Rat.divInt_ofNat (num : Int) (den : Nat) :

Rat.divInt num ↑den = mkRat num den

source

theorem Rat.mk_eq_divInt (num : Int) (den : Nat) (nz : den ≠ 0) (c : num.natAbs.Coprime den) :

{ num := num, den := den, den_nz := nz, reduced := c } = Rat.divInt num ↑den

source

theorem Rat.divInt_self (a : Rat) :

Rat.divInt a.num ↑a.den = a

source

@[simp]

theorem Rat.zero_divInt (n : Int) :

Rat.divInt 0 n = 0

source

@[simp]

theorem Rat.divInt_zero (n : Int) :

Rat.divInt n 0 = 0

source

theorem Rat.neg_divInt_neg (num : Int) (den : Int) :

Rat.divInt (-num) (-den) = Rat.divInt num den

source

theorem Rat.divInt_neg' (num : Int) (den : Int) :

Rat.divInt num (-den) = Rat.divInt (-num) den

source

theorem Rat.divInt_eq_iff {d₁ : Int} {d₂ : Int} {n₁ : Int} {n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :

Rat.divInt n₁ d₁ = Rat.divInt n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

source

theorem Rat.divInt_mul_left {n : Int} {d : Int} {a : Int} (a0 : a ≠ 0) :

Rat.divInt (a * n) (a * d) = Rat.divInt n d

source

theorem Rat.divInt_mul_right {n : Int} {d : Int} {a : Int} (a0 : a ≠ 0) :

Rat.divInt (n * a) (d * a) = Rat.divInt n d

source

theorem Rat.divInt_num_den {d : Int} {n : Int} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'} (z : d ≠ 0) (h : Rat.divInt n d = { num := n', den := d', den_nz := z', reduced := c }) :

∃ (m : Int), m ≠ 0 ∧ n = n' * m ∧ d = ↑d' * m

source

@[simp]

theorem Rat.ofInt_ofNat {n : Nat} :

Rat.ofInt (OfNat.ofNat n) = OfNat.ofNat n

source

@[simp]

theorem Rat.ofInt_num {n : Int} :

(Rat.ofInt n).num = n

source

@[simp]

theorem Rat.ofInt_den {n : Int} :

(Rat.ofInt n).den = 1

source

@[simp]

theorem Rat.ofNat_num {n : Nat} :

Rat.num (OfNat.ofNat n) = OfNat.ofNat n

source

@[simp]

theorem Rat.ofNat_den {n : Nat} :

Rat.den (OfNat.ofNat n) = 1

source

theorem Rat.add_def (a : Rat) (b : Rat) :

a + b = Rat.normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

source

theorem Rat.add_def' (a : Rat) (b : Rat) :

a + b = mkRat (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)

source

theorem Rat.normalize_add_normalize (n₁ : Int) (n₂ : Int) {d₁ : Nat} {d₂ : Nat} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :

Rat.normalize n₁ d₁ z₁ + Rat.normalize n₂ d₂ z₂ = Rat.normalize (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂) ⋯

source

theorem Rat.mkRat_add_mkRat (n₁ : Int) (n₂ : Int) {d₁ : Nat} {d₂ : Nat} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :

mkRat n₁ d₁ + mkRat n₂ d₂ = mkRat (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂)

source

theorem Rat.divInt_add_divInt (n₁ : Int) (n₂ : Int) {d₁ : Int} {d₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :

Rat.divInt n₁ d₁ + Rat.divInt n₂ d₂ = Rat.divInt (n₁ * d₂ + n₂ * d₁) (d₁ * d₂)

source

@[simp]

theorem Rat.neg_num (a : Rat) :

(-a).num = -a.num

source

@[simp]

theorem Rat.neg_den (a : Rat) :

(-a).den = a.den

source

theorem Rat.neg_normalize (n : Int) (d : Nat) (z : d ≠ 0) :

-Rat.normalize n d z = Rat.normalize (-n) d z

source

theorem Rat.neg_mkRat (n : Int) (d : Nat) :

-mkRat n d = mkRat (-n) d

source

theorem Rat.neg_divInt (n : Int) (d : Int) :

-Rat.divInt n d = Rat.divInt (-n) d

source

theorem Rat.sub_def (a : Rat) (b : Rat) :

a - b = Rat.normalize (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den) ⋯

source

theorem Rat.sub_def' (a : Rat) (b : Rat) :

a - b = mkRat (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den)

source

theorem Rat.sub_eq_add_neg (a : Rat) (b : Rat) :

a - b = a + -b

source

theorem Rat.divInt_sub_divInt (n₁ : Int) (n₂ : Int) {d₁ : Int} {d₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :

Rat.divInt n₁ d₁ - Rat.divInt n₂ d₂ = Rat.divInt (n₁ * d₂ - n₂ * d₁) (d₁ * d₂)

source

theorem Rat.mul_def (a : Rat) (b : Rat) :

a * b = Rat.normalize (a.num * b.num) (a.den * b.den) ⋯

source

theorem Rat.mul_comm (a : Rat) (b : Rat) :

a * b = b * a

source

@[simp]

theorem Rat.zero_mul (a : Rat) :

0 * a = 0

source

@[simp]

theorem Rat.mul_zero (a : Rat) :

a * 0 = 0

source

@[simp]

theorem Rat.one_mul (a : Rat) :

1 * a = a

source

@[simp]

theorem Rat.mul_one (a : Rat) :

a * 1 = a

source

theorem Rat.normalize_mul_normalize (n₁ : Int) (n₂ : Int) {d₁ : Nat} {d₂ : Nat} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :

Rat.normalize n₁ d₁ z₁ * Rat.normalize n₂ d₂ z₂ = Rat.normalize (n₁ * n₂) (d₁ * d₂) ⋯

source

theorem Rat.mkRat_mul_mkRat (n₁ : Int) (n₂ : Int) (d₁ : Nat) (d₂ : Nat) :

mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)

source

theorem Rat.divInt_mul_divInt (n₁ : Int) (n₂ : Int) {d₁ : Int} {d₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) :

Rat.divInt n₁ d₁ * Rat.divInt n₂ d₂ = Rat.divInt (n₁ * n₂) (d₁ * d₂)

source

theorem Rat.inv_def (a : Rat) :

a.inv = Rat.divInt (↑a.den) a.num

source

@[simp]

theorem Rat.inv_zero :

Rat.inv 0 = 0

source

@[simp]

theorem Rat.inv_divInt (n : Int) (d : Int) :

(Rat.divInt n d).inv = Rat.divInt d n

source

theorem Rat.div_def (a : Rat) (b : Rat) :

a / b = a * b.inv

source

theorem Rat.ofScientific_true_def {m : Nat} {e : Nat} :

Rat.ofScientific m true e = mkRat (↑m) (10 ^ e)

source

theorem Rat.ofScientific_false_def {m : Nat} {e : Nat} :

Rat.ofScientific m false e = ↑(m * 10 ^ e)

source

theorem Rat.ofScientific_def {m : Nat} {s : Bool} {e : Nat} :

Rat.ofScientific m s e = if s = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)

source

@[simp]

theorem Rat.intCast_den (a : Int) :

(↑a).den = 1

source

@[simp]

theorem Rat.intCast_num (a : Int) :

(↑a).num = a

The following lemmas are later subsumed by e.g. Int.cast_add and Int.cast_mul in Mathlib but it is convenient to have these earlier, for users who only need Int and Rat.

source

@[simp]

theorem Rat.intCast_inj {a : Int} {b : Int} :

↑a = ↑b ↔ a = b

source

theorem Rat.intCast_zero :

↑0 = 0

source

theorem Rat.intCast_one :

↑1 = 1

source

@[simp]