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

• Rat.divInt n d constructs a rational number q = n / d from n d : ℤ.

Notations

• /. is infix notation for Rat.divInt.

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 : ℕ) : (OfNat.ofNat n).num = OfNat.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

theorem Rat.intCast_injective : Function.Injective Int.cast

theorem Rat.natCast_injective : Function.Injective Nat.cast

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

theorem Rat.intCast_eq_divInt (z : ℤ) : ↑z = Rat.divInt z 1

@[simp]

theorem Rat.divInt_self' {n : ℤ} (hn : n ≠ 0) : Rat.divInt n n = 1

def Rat.numDenCasesOn {C : ℚ → Sort u} (a : ℚ) : ((n : ℤ) → (d : ℕ) → 0 < d → n.natAbs.Coprime d → C (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

• { num := n, den := d, den_nz := h, reduced := c }.numDenCasesOn x✝ = ⋯.mpr (x✝ n d ⋯ c)

def Rat.numDenCasesOn' {C : ℚ → Sort u} (a : ℚ) (H : (n : ℤ) → (d : ℕ) → d ≠ 0 → C (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 ⋯

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

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₁ ≠ 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.divInt a b) (Rat.divInt c d) = Rat.divInt (f₁ a b c d) (f₂ a b c d)

theorem Rat.neg_def (q : ℚ) : -q = Rat.divInt (-q.num) ↑q.den

@[simp]

theorem Rat.divInt_neg (n d : ℤ) : Rat.divInt n (-d) = Rat.divInt (-n) 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.

instance Rat.instPowNat : Pow ℚ ℕ

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 : Inv ℚ

Equations

• Rat.instInv = { inv := Rat.inv }

@[simp]

theorem Rat.inv_divInt' (a b : ℤ) : (Rat.divInt a b)⁻¹ = Rat.divInt b a

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

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

@[simp]

theorem Rat.divInt_one (n : ℤ) : Rat.divInt n 1 = ↑n

@[simp]

theorem Rat.mkRat_one (n : ℤ) : mkRat n 1 = ↑n

theorem Rat.divInt_one_one : Rat.divInt 1 1 = 1

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.zero_ne_one : 0 ≠ 1

theorem Rat.mul_inv_cancel (a : ℚ) : a ≠ 0 → a * a⁻¹ = 1

theorem Rat.inv_mul_cancel (a : ℚ) (h : a ≠ 0) : a⁻¹ * a = 1

instance Rat.nontrivial : Nontrivial ℚ

The rational numbers are a group

instance Rat.addCommGroup : AddCommGroup ℚ

Equations

• Rat.addCommGroup = AddCommGroup.mk Rat.add_comm

instance Rat.addGroup : AddGroup ℚ

Equations

• Rat.addGroup = inferInstance

instance Rat.addCommMonoid : AddCommMonoid ℚ

Equations

• Rat.addCommMonoid = inferInstance

instance Rat.addMonoid : AddMonoid ℚ

Equations

• Rat.addMonoid = inferInstance

instance Rat.addLeftCancelSemigroup : AddLeftCancelSemigroup ℚ

Equations

• Rat.addLeftCancelSemigroup = inferInstance

instance Rat.addRightCancelSemigroup : AddRightCancelSemigroup ℚ

Equations

• Rat.addRightCancelSemigroup = inferInstance

instance Rat.addCommSemigroup : AddCommSemigroup ℚ

Equations

• Rat.addCommSemigroup = inferInstance

instance Rat.addSemigroup : AddSemigroup ℚ

Equations

• Rat.addSemigroup = inferInstance

instance Rat.commMonoid : CommMonoid ℚ

Equations

• Rat.commMonoid = CommMonoid.mk Rat.mul_comm

instance Rat.monoid : Monoid ℚ

Equations

• Rat.monoid = inferInstance

instance Rat.commSemigroup : CommSemigroup ℚ

Equations

• Rat.commSemigroup = inferInstance

instance Rat.semigroup : Semigroup ℚ

Equations

• Rat.semigroup = inferInstance

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

theorem Rat.num_zero : Rat.num 0 = 0

theorem Rat.den_zero : Rat.den 0 = 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_one : Rat.num 1 = 1

@[simp]

theorem Rat.den_one : Rat.den 1 = 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) : Rat.divInt n d ≠ 0

theorem Rat.nonneg_antisymm {q : ℚ} : 0 ≤ q → 0 ≤ -q → q = 0

theorem Rat.nonneg_total (a : ℚ) : 0 ≤ a ∨ 0 ≤ -a

theorem Rat.add_divInt (a b c : ℤ) : Rat.divInt (a + b) c = Rat.divInt a c + Rat.divInt 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 : ℤ) : Rat.divInt n x * Rat.divInt x d = Rat.divInt 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

theorem Rat.coe_int_inj (m n : ℤ) : ↑m = ↑n ↔ m = n