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
theorem Rat.mk'_num_den (q : ) :
{ num := q.num, den := q.den, den_nz := , reduced := } = q
@[simp]
theorem Rat.ofInt_eq_cast (n : ) :
Rat.ofInt n = n
@[simp]
theorem Rat.num_ofNat (n : ) :
@[simp]
theorem Rat.den_ofNat (n : ) :
(OfNat.ofNat n).den = 1
@[simp]
theorem Rat.num_natCast (n : ) :
(↑n).num = n
@[simp]
theorem Rat.den_natCast (n : ) :
(↑n).den = 1
@[simp]
theorem Rat.num_intCast (n : ) :
(↑n).num = n
@[simp]
theorem Rat.den_intCast (n : ) :
(↑n).den = 1
@[deprecated Rat.num_intCast]
theorem Rat.coe_int_num (n : ) :
(↑n).num = n

Alias of Rat.num_intCast.

@[deprecated Rat.den_intCast]
theorem Rat.coe_int_den (n : ) :
(↑n).den = 1

Alias of Rat.den_intCast.

@[simp]
theorem Rat.natCast_inj {m : } {n : } :
m = n m = n
@[simp]
theorem Rat.intCast_eq_zero {n : } :
n = 0 n = 0
@[simp]
theorem Rat.natCast_eq_zero {n : } :
n = 0 n = 0
@[simp]
theorem Rat.intCast_eq_one {n : } :
n = 1 n = 1
@[simp]
theorem Rat.natCast_eq_one {n : } :
n = 1 n = 1
theorem Rat.mkRat_eq_divInt (n : ) (d : ) :
mkRat n d = Rat.divInt n d
@[simp]
theorem Rat.mk'_zero (d : ) (h : d 0) (w : (Int.natAbs 0).Coprime d) :
{ num := 0, den := d, den_nz := h, reduced := w } = 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.den_ne_zero (q : ) :
q.den 0
@[simp]
theorem Rat.num_nonneg {q : } :
0 q.num 0 q
@[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 : n.natAbs.gcd d = 1) :
Rat.normalize n d h = { num := n, den := d, den_nz := h, reduced := c }
@[simp]
theorem Rat.mkRat_num_den' (a : ) :
mkRat a.num a.den = a

Alias of Rat.mkRat_self.

theorem Rat.num_divInt_den (q : ) :
Rat.divInt q.num q.den = q
theorem Rat.mk'_eq_divInt {n : } {d : } {h : d 0} {c : n.natAbs.Coprime d} :
{ num := n, den := d, den_nz := h, reduced := c } = Rat.divInt n d
@[simp]
theorem Rat.divInt_self' {n : } (hn : n 0) :
def Rat.numDenCasesOn {C : Sort u} (a : ) :
((n : ) → (d : ) → 0 < dn.natAbs.Coprime 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
  • x✝.numDenCasesOn x = match x✝, x with | { num := n, den := d, den_nz := h, reduced := c }, H => .mpr (H n d c)
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
    • a.numDenCasesOn' H = a.numDenCasesOn fun (n : ) (d : ) (h : 0 < d) (x : n.natAbs.Coprime d) => H n d
    Instances For
      def Rat.numDenCasesOn'' {C : Sort u} (a : ) (H : (n : ) → (d : ) → (nz : d 0) → (red : n.natAbs.Coprime d) → C { num := n, den := d, den_nz := nz, reduced := red }) :
      C a

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

      Equations
      • a.numDenCasesOn'' H = a.numDenCasesOn fun (n : ) (d : ) (h : 0 < d) (h' : n.natAbs.Coprime d) => .mpr (H n d h')
      Instances For
        theorem Rat.lift_binop_eq (f : ) (f₁ : ) (f₂ : ) (fv : ∀ {n₁ : } {d₁ : } {h₁ : d₁ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : } {d₂ : } {h₂ : d₂ 0} {c₂ : n₂.natAbs.Coprime d₂}, f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } = 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)
        @[deprecated Rat.divInt_add_divInt]
        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)
        theorem Rat.neg_def (q : ) :
        -q = Rat.divInt (-q.num) q.den
        @[simp]
        theorem Rat.divInt_neg (n : ) (d : ) :
        @[deprecated Rat.divInt_neg]
        theorem Rat.divInt_neg_den (n : ) (d : ) :

        Alias of Rat.divInt_neg.

        @[deprecated Rat.divInt_sub_divInt]
        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.divInt_mul_divInt' (n₁ : ) (d₁ : ) (n₂ : ) (d₂ : ) :
        Rat.divInt n₁ d₁ * Rat.divInt n₂ d₂ = Rat.divInt (n₁ * n₂) (d₁ * d₂)
        theorem Rat.mk'_mul_mk' (n₁ : ) (n₂ : ) (d₁ : ) (d₂ : ) (hd₁ : d₁ 0) (hd₂ : d₂ 0) (hnd₁ : n₁.natAbs.Coprime d₁) (hnd₂ : n₂.natAbs.Coprime d₂) (h₁₂ : n₁.natAbs.Coprime d₂) (h₂₁ : n₂.natAbs.Coprime d₁) :
        { num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ } * { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ } = { num := n₁ * n₂, den := d₁ * d₂, den_nz := , reduced := }
        theorem Rat.mul_eq_mkRat (q : ) (r : ) :
        q * r = mkRat (q.num * r.num) (q.den * r.den)
        theorem Rat.divInt_eq_divInt {d₁ : } {d₂ : } {n₁ : } {n₂ : } (z₁ : d₁ 0) (z₂ : d₂ 0) :
        Rat.divInt n₁ d₁ = Rat.divInt n₂ d₂ n₁ * d₂ = n₂ * d₁

        Alias of Rat.divInt_eq_iff.

        @[deprecated Rat.mul_eq_mkRat]
        theorem Rat.mul_num_den (q : ) (r : ) :
        q * r = mkRat (q.num * r.num) (q.den * r.den)

        Alias of Rat.mul_eq_mkRat.

        Equations
        • Rat.instPowNat = { pow := fun (q : ) (n : ) => { num := q.num ^ n, den := q.den ^ n, den_nz := , reduced := } }
        theorem Rat.pow_def (q : ) (n : ) :
        q ^ n = { num := q.num ^ n, den := q.den ^ n, den_nz := , reduced := }
        theorem Rat.pow_eq_mkRat (q : ) (n : ) :
        q ^ n = mkRat (q.num ^ n) (q.den ^ n)
        theorem Rat.pow_eq_divInt (q : ) (n : ) :
        q ^ n = Rat.divInt (q.num ^ n) (q.den ^ n)
        @[simp]
        theorem Rat.num_pow (q : ) (n : ) :
        (q ^ n).num = q.num ^ n
        @[simp]
        theorem Rat.den_pow (q : ) (n : ) :
        (q ^ n).den = q.den ^ n
        @[simp]
        theorem Rat.mk'_pow (num : ) (den : ) (hd : den 0) (hdn : num.natAbs.Coprime den) (n : ) :
        { num := num, den := den, den_nz := hd, reduced := hdn } ^ n = { num := num ^ n, den := den ^ n, den_nz := , reduced := }
        instance Rat.instInv :
        Equations
        @[simp]
        theorem Rat.inv_divInt' (a : ) (b : ) :
        @[simp]
        theorem Rat.inv_mkRat (a : ) (b : ) :
        (mkRat a b)⁻¹ = Rat.divInt (↑b) a
        theorem Rat.inv_def' (q : ) :
        q⁻¹ = Rat.divInt (↑q.den) q.num
        @[simp]
        theorem Rat.divInt_div_divInt (n₁ : ) (d₁ : ) (n₂ : ) (d₂ : ) :
        Rat.divInt n₁ d₁ / Rat.divInt n₂ d₂ = Rat.divInt (n₁ * d₂) (d₁ * n₂)
        theorem Rat.div_def' (q : ) (r : ) :
        q / r = Rat.divInt (q.num * r.den) (q.den * r.num)
        @[deprecated Rat.div_def']
        theorem Rat.div_num_den (q : ) (r : ) :
        q / r = Rat.divInt (q.num * r.den) (q.den * r.num)

        Alias of Rat.div_def'.

        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.neg_add_cancel (a : ) :
        -a + a = 0
        @[deprecated Rat.zero_divInt]
        @[simp]
        theorem Rat.divInt_one (n : ) :
        Rat.divInt n 1 = n
        @[simp]
        theorem Rat.mkRat_one (n : ) :
        mkRat n 1 = n
        @[deprecated Rat.divInt_one]
        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

        The rational numbers are a group #

        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 :
        @[simp]
        theorem Rat.den_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
        @[simp]
        theorem Rat.num_one :
        @[simp]
        theorem Rat.den_one :
        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.nonneg_antisymm {q : } :
        0 q0 -qq = 0
        theorem Rat.nonneg_total (a : ) :
        0 a 0 -a
        theorem Rat.add_divInt (a : ) (b : ) (c : ) :
        theorem Rat.divInt_eq_div (n : ) (d : ) :
        Rat.divInt n d = n / d
        theorem Rat.intCast_div_eq_divInt (n : ) (d : ) :
        n / d = Rat.divInt n d
        theorem Rat.natCast_div_eq_divInt (n : ) (d : ) :
        n / d = Rat.divInt n d
        theorem Rat.divInt_mul_divInt_cancel {x : } (hx : x 0) (n : ) (d : ) :
        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 : q.isInt = 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
        @[deprecated Rat.intCast_eq_divInt]
        theorem Rat.coe_int_eq_divInt (z : ) :
        z = Rat.divInt z 1

        Alias of Rat.intCast_eq_divInt.

        @[deprecated Rat.intCast_div_eq_divInt]
        theorem Rat.coe_int_div_eq_divInt (n : ) (d : ) :
        n / d = Rat.divInt n d

        Alias of Rat.intCast_div_eq_divInt.

        theorem Rat.coe_int_inj (m : ) (n : ) :
        m = n m = n