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.

source

theorem Rat.pos (a : ℚ) :

0 < a.den

source

@[simp]

theorem Rat.ofInt_eq_cast (n : ℤ) :

Rat.ofInt n = ↑n

source

@[simp]

theorem Rat.num_ofNat (n : ℕ) :

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

source

@[simp]

theorem Rat.den_ofNat (n : ℕ) :

(OfNat.ofNat n).den = 1

source

@[simp]

theorem Rat.coe_int_num (n : ℤ) :

(↑n).num = n

source

@[simp]

theorem Rat.coe_int_den (n : ℤ) :

(↑n).den = 1

source

theorem Rat.mkRat_eq (n : ℤ) (d : ℕ) :

mkRat n d = Rat.divInt n ↑d

source

@[simp]

theorem Rat.zero_mk (d : ℕ) (h : d ≠ 0) (w : Nat.Coprime (Int.natAbs 0) d) :

{ num := 0, den := d, den_nz := h, reduced := w } = 0

source

@[simp]

theorem Rat.num_eq_zero {q : ℚ} :

q.num = 0 ↔ q = 0

source

theorem Rat.num_ne_zero {q : ℚ} :

q.num ≠ 0 ↔ q ≠ 0

source

@[simp]

theorem Rat.divInt_eq_zero {a : ℤ} {b : ℤ} (b0 : b ≠ 0) :

Rat.divInt a b = 0 ↔ a = 0

source

theorem Rat.divInt_ne_zero {a : ℤ} {b : ℤ} (b0 : b ≠ 0) :

Rat.divInt a b ≠ 0 ↔ a ≠ 0

source

theorem Rat.normalize_eq_mk' (n : ℤ) (d : ℕ) (h : d ≠ 0) (c : Nat.gcd (Int.natAbs n) d = 1) :

Rat.normalize n d h = { num := n, den := d, den_nz := h, reduced := c }

source

theorem Rat.num_den {a : ℚ} :

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

source

theorem Rat.num_den' {n : ℤ} {d : ℕ} {h : d ≠ 0} {c : Nat.Coprime (Int.natAbs n) d} :

{ num := n, den := d, den_nz := h, reduced := c } = Rat.divInt n ↑d

source

theorem Rat.coe_int_eq_divInt (z : ℤ) :

↑z = Rat.divInt z 1

source

def Rat.numDenCasesOn {C : ℚ → Sort u} (a : ℚ) :

((n : ℤ) → (d : ℕ) → 0 < d → Nat.Coprime (Int.natAbs n) 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

Rat.numDenCasesOn x✝ x = match x✝, x with | { num := n, den := d, den_nz := h, reduced := c }, H => Eq.mpr ⋯ (H n d ⋯ c)

Instances For

source

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

Rat.numDenCasesOn' a H = Rat.numDenCasesOn a fun (n : ℤ) (d : ℕ) (h : 0 < d) (x : Nat.Coprime (Int.natAbs n) d) => H n d ⋯

Instances For

source

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

source

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

source

@[simp]

theorem Rat.neg_def {a : ℤ} {b : ℤ} :

-Rat.divInt a b = Rat.divInt (-a) b

source

@[simp]

theorem Rat.divInt_neg_den (n : ℤ) (d : ℤ) :

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

source

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

source

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

source

instance Rat.instInvRat :

Inv ℚ

Equations

Rat.instInvRat = { inv := Rat.inv }

source

@[simp]

theorem Rat.inv_def' {a : ℤ} {b : ℤ} :

(Rat.divInt a b)⁻¹ = Rat.divInt b a

source

theorem Rat.add_zero (a : ℚ) :

a + 0 = a

source

theorem Rat.zero_add (a : ℚ) :

0 + a = a

source

theorem Rat.add_comm (a : ℚ) (b : ℚ) :

a + b = b + a

source

theorem Rat.add_assoc (a : ℚ) (b : ℚ) (c : ℚ) :

a + b + c = a + (b + c)

source

theorem Rat.add_left_neg (a : ℚ) :

-a + a = 0

source

theorem Rat.divInt_zero_one :

Rat.divInt 0 1 = 0

source

@[simp]

theorem Rat.divInt_one_one :

Rat.divInt 1 1 = 1

source

@[simp]

theorem Rat.divInt_neg_one_one :

Rat.divInt (-1) 1 = -1

source

theorem Rat.divInt_one (n : ℤ) :

Rat.divInt n 1 = ↑n

source

theorem Rat.mkRat_one {n : ℤ} :

mkRat n 1 = ↑n

source

theorem Rat.mul_assoc (a : ℚ) (b : ℚ) (c : ℚ) :

a * b * c = a * (b * c)

source

theorem Rat.add_mul (a : ℚ) (b : ℚ) (c : ℚ) :

(a + b) * c = a * c + b * c

source

theorem Rat.mul_add (a : ℚ) (b : ℚ) (c : ℚ) :

a * (b + c) = a * b + a * c

source

theorem Rat.zero_ne_one :

0 ≠ 1

source

theorem Rat.mul_inv_cancel (a : ℚ) :

a ≠ 0 → a * a⁻¹ = 1

source

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.

source

instance Rat.commRing :

CommRing ℚ

Equations