Documentation

Mathlib.Data.Rat.Defs

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 #

Notations #

theorem Rat.pos (a : ) :
0 < a.den
@[simp]
theorem Rat.ofInt_eq_cast (n : ) :
Rat.ofInt n = n
@[simp]
theorem Rat.coe_int_num (n : ) :
(n).num = n
@[simp]
theorem Rat.coe_int_den (n : ) :
(n).den = 1
theorem Rat.mkRat_eq (n : ) (d : ) :
mkRat n d = Rat.divInt n d
@[simp]
theorem Rat.zero_mk (d : ) (h : d 0) (w : Nat.coprime (Int.natAbs 0) d) :
Rat.mk' 0 d = 0
@[simp]
theorem Rat.divInt_eq_zero {a : } {b : } (b0 : b 0) :
Rat.divInt a b = 0 a = 0
theorem Rat.divInt_ne_zero {a : } {b : } (b0 : b 0) :
Rat.divInt a b 0 a 0
theorem Rat.normalize_eq_mk' (n : ) (d : ) (h : d 0) (c : Nat.gcd (Int.natAbs n) d = 1) :
theorem Rat.num_den {a : } :
Rat.divInt a.num a.den = a
theorem Rat.num_den' {n : } {d : } {h : d 0} {c : Nat.coprime (Int.natAbs n) d} :
Rat.mk' n d = Rat.divInt n d
def Rat.numDenCasesOn {C : Sort u} (a : ) :
((n : ) → (d : ) → 0 < dNat.coprime (Int.natAbs n) dC (Rat.divInt n d)) → C a

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

Equations
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∀ r : ℚ, p r by dealing with rational numbers of the form n /. d with d ≠ 0≠ 0.

Equations
theorem Rat.lift_binop_eq (f : ) (f₁ : ) (f₂ : ) (fv : ∀ {n₁ : } {d₁ : } {h₁ : d₁ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : } {d₂ : } {h₂ : d₂ 0} {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (Rat.mk' n₁ d₁) (Rat.mk' n₂ d₂) = 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)
@[simp]
theorem Rat.add_def'' {a : } {b : } {c : } {d : } (b0 : b 0) (d0 : d 0) :
Rat.divInt a b + Rat.divInt c d = Rat.divInt (a * d + c * b) (b * d)
@[simp]
theorem Rat.neg_def {a : } {b : } :
@[simp]
theorem Rat.divInt_neg_den (n : ) (d : ) :
@[simp]
theorem Rat.sub_def'' {a : } {b : } {c : } {d : } (b0 : b 0) (d0 : d 0) :
Rat.divInt a b - Rat.divInt c d = Rat.divInt (a * d - c * b) (b * d)
@[simp]
theorem Rat.mul_def' {a : } {b : } {c : } {d : } (b0 : b 0) (d0 : d 0) :
Rat.divInt a b * Rat.divInt c d = Rat.divInt (a * c) (b * d)
Equations
@[simp]
theorem Rat.inv_def' {a : } {b : } :
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_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

At this point in the import hierarchy we have not defined the Field typeclass. Instead we'll instantiate CommRing and CommGroupWithZero at this point. The Rat.field instance and any field-specific lemmas can be found in Mathlib.Data.Rat.Basic.

Equations
Equations
Equations
Equations
Equations
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.num = 0
@[simp]
theorem Rat.den_zero :
0.den = 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
theorem Rat.num_ne_zero_of_ne_zero {q : } (h : q 0) :
q.num 0
@[simp]
theorem Rat.num_one :
1.num = 1
@[simp]
theorem Rat.den_one :
1.den = 1
theorem Rat.mk_num_ne_zero_of_ne_zero {q : } {n : } {d : } (hq : q 0) (hqnd : q = Rat.divInt n d) :
n 0
theorem Rat.mk_denom_ne_zero_of_ne_zero {q : } {n : } {d : } (hq : q 0) (hqnd : q = Rat.divInt n d) :
d 0
theorem Rat.divInt_ne_zero_of_ne_zero {n : } {d : } (h : n 0) (hd : d 0) :
theorem Rat.mul_num_den (q : ) (r : ) :
q * r = Rat.divInt (q.num * r.num) ↑(q.den * r.den)
theorem Rat.div_num_den (q : ) (r : ) :
q / r = Rat.divInt (q.num * r.den) (q.den * r.num)
theorem Rat.add_divInt (a : ) (b : ) (c : ) :
theorem Rat.divInt_eq_div (n : ) (d : ) :
Rat.divInt n d = n / d
theorem Rat.divInt_mul_divInt_cancel {x : } (hx : x 0) (n : ) (d : ) :
theorem Rat.divInt_div_divInt_cancel_left {x : } (hx : x 0) (n : ) (d : ) :
theorem Rat.divInt_div_divInt_cancel_right {x : } (hx : x 0) (n : ) (d : ) :
theorem Rat.coe_int_div_eq_divInt {n : } {d : } :
n / d = Rat.divInt n d
theorem Rat.num_div_den (r : ) :
r.num / r.den = r
theorem Rat.coe_int_num_of_den_eq_one {q : } (hq : q.den = 1) :
q.num = q
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
theorem Rat.coe_nat_eq_divInt (n : ) :
n = Rat.divInt (n) 1
@[simp]
theorem Rat.coe_nat_num (n : ) :
(n).num = n
@[simp]
theorem Rat.coe_nat_den (n : ) :
(n).den = 1
theorem Rat.coe_int_inj (m : ) (n : ) :
m = n m = n