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.num_eq_zero {q : } :
q.num = 0 q = 0
theorem Rat.num_ne_zero {q : } :
q.num 0 q 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 by dealing with rational numbers of the form n /. d with 0 < d and coprime n, d.

Equations
Instances For
    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 by dealing with rational numbers of the form n /. d with d ≠ 0.

    Equations
    Instances For
      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
      @[simp]
      theorem Rat.divInt_one (n : ) :
      Rat.divInt n 1 = n
      theorem Rat.mkRat_one {n : } :
      mkRat n 1 = n
      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
      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.eq_num_of_isInt {q : } (h : Rat.isInt q = true) :
      q = q.num
      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
      theorem Rat.mkRat_eq_div {n : } {d : } :
      mkRat n d = n / d