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/Algebra/Field/Rat.lean once the Field class has been defined.

Main Definitions #

Notation #

source
theorem Rat.pos (a : ℚ) :
0 < a.den
source
theorem Rat.mk'_num_den (q : ℚ) :
{ num := q.num, den := q.den, den_nz := ⋯, reduced := ⋯ } = q
source
@[simp]
theorem Rat.ofInt_eq_cast (n : ℤ) :
ofInt n = ↑n
source
theorem Rat.intCast_injective :
Function.Injective Int.cast
source
theorem Rat.natCast_injective :
Function.Injective Nat.cast
source
@[deprecated Rat.intCast_eq_zero_iff (since := "2025-10-24")]
theorem Rat.intCast_eq_zero {a : ℤ} :
↑a = 0 ↔ a = 0

Alias of Rat.intCast_eq_zero_iff.

source
@[deprecated Rat.natCast_eq_zero_iff (since := "2025-10-24")]
theorem Rat.natCast_eq_zero {a : ℕ} :
↑a = 0 ↔ a = 0

Alias of Rat.natCast_eq_zero_iff.

source
@[simp]
theorem Rat.intCast_eq_one_iff {n : ℤ} :
↑n = 1 ↔ n = 1
source
@[deprecated Rat.intCast_eq_one_iff (since := "2025-10-24")]
theorem Rat.intCast_eq_one {n : ℤ} :
↑n = 1 ↔ n = 1

Alias of Rat.intCast_eq_one_iff.

source
@[simp]
theorem Rat.natCast_eq_one_iff {n : ℕ} :
↑n = 1 ↔ n = 1
source
@[deprecated Rat.natCast_eq_one_iff (since := "2025-10-24")]
theorem Rat.natCast_eq_one {n : ℕ} :
↑n = 1 ↔ n = 1

Alias of Rat.natCast_eq_one_iff.

source
theorem Rat.mkRat_eq_divInt (n : ℤ) (d : ℕ) :
mkRat n d = divInt n ↑d
source
@[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
source
theorem Rat.num_ne_zero {q : ℚ} :
q.num ≠ 0 ↔ q ≠ 0
source
@[simp]
theorem Rat.den_ne_zero (q : ℚ) :
q.den ≠ 0
source
@[simp]
theorem Rat.divInt_eq_zero {a b : ℤ} (b0 : b ≠ 0) :
divInt a b = 0 ↔ a = 0
source
theorem Rat.divInt_ne_zero {a b : ℤ} (b0 : b ≠ 0) :
divInt a b ≠ 0 ↔ a ≠ 0
source
theorem Rat.mkRat_num_den' (a : ℚ) :
mkRat a.num a.den = a

Alias of Rat.mkRat_self.

source
theorem Rat.intCast_eq_divInt (z : ℤ) :
↑z = divInt z 1
source
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₂ } = 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 (divInt a b) (divInt c d) = divInt (f₁ a b c d) (f₂ a b c d)
source
theorem Rat.neg_def (q : ℚ) :
-q = divInt (-q.num) ↑q.den
source
@[simp]
theorem Rat.divInt_neg (n d : ℤ) :
divInt n (-d) = divInt (-n) d
source
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 := ⋯ }
source
theorem Rat.mul_eq_mkRat (q r : ℚ) :
q * r = mkRat (q.num * r.num) (q.den * r.den)
source
theorem Rat.pow_eq_mkRat (q : ℚ) (n : ℕ) :
q ^ n = mkRat (q.num ^ n) (q.den ^ n)
source
theorem Rat.pow_eq_divInt (q : ℚ) (n : ℕ) :
q ^ n = divInt (q.num ^ n) (↑q.den ^ n)
source
@[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 := ⋯ }
source
@[simp]
theorem Rat.inv_mkRat (a : ℤ) (b : ℕ) :
(mkRat a b)⁻¹ = divInt (↑b) a
source
@[simp]
theorem Rat.divInt_div_divInt (n₁ d₁ n₂ d₂ : ℤ) :
divInt n₁ d₁ / divInt n₂ d₂ = divInt (n₁ * d₂) (d₁ * n₂)
source
theorem Rat.div_def' (q r : ℚ) :
q / r = divInt (q.num * ↑r.den) (↑q.den * r.num)
source
@[simp]
theorem Rat.divInt_one (n : ℤ) :
divInt n 1 = ↑n
source
theorem Rat.divInt_one_one :
divInt 1 1 = 1
source
theorem Rat.zero_ne_one :
0 ≠ 1
source
📐 coverage
instance Rat.nontrivial :
Nontrivial ℚ

The rational numbers are a group #

source
🔸 coverage
@[implicit_reducible]
instance Rat.addCommGroup :
AddCommGroup ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.addGroup :
AddGroup ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.addCommMonoid :
AddCommMonoid ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.addMonoid :
AddMonoid ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.addLeftCancelSemigroup :
AddLeftCancelSemigroup ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.addRightCancelSemigroup :
AddRightCancelSemigroup ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.addCommSemigroup :
AddCommSemigroup ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.addSemigroup :
AddSemigroup ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.commMonoid :
CommMonoid ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.monoid :
Monoid ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.commSemigroup :
CommSemigroup ℚ
source
🔸 coverage
@[implicit_reducible]
instance Rat.semigroup :
Semigroup ℚ
source
@[simp]
theorem Rat.den_neg_eq_den (q : ℚ) :
(-q).den = q.den
source
@[simp]
theorem Rat.num_neg_eq_neg_num (q : ℚ) :
(-q).num = -q.num
source
theorem Rat.num_zero :
num 0 = 0
source
theorem Rat.den_zero :
den 0 = 1
source
theorem Rat.zero_of_num_zero {q : ℚ} (hq : q.num = 0) :
q = 0
source
theorem Rat.zero_iff_num_zero {q : ℚ} :
q = 0 ↔ q.num = 0
source
theorem Rat.num_one :
num 1 = 1
source
@[simp]
theorem Rat.den_one :
den 1 = 1
source
theorem Rat.mk_num_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = divInt n d) :
n ≠ 0
source
theorem Rat.mk_denom_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = divInt n d) :
d ≠ 0
source
theorem Rat.divInt_ne_zero_of_ne_zero {n d : ℤ} (h : n ≠ 0) (hd : d ≠ 0) :
divInt n d ≠ 0
source
theorem Rat.add_divInt (a b c : ℤ) :
divInt (a + b) c = divInt a c + divInt b c
source
theorem Rat.intCast_div_eq_divInt (n d : ℤ) :
↑n / ↑d = divInt n d
source
theorem Rat.natCast_div_eq_divInt (n d : ℕ) :
↑n / ↑d = divInt ↑n ↑d
source
theorem Rat.divInt_mul_divInt_cancel {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :
divInt n x * divInt x d = divInt n d
source
theorem Rat.coe_int_num_of_den_eq_one {q : ℚ} (hq : q.den = 1) :
↑q.num = q
source
theorem Rat.eq_num_of_isInt {q : ℚ} (h : q.isInt = true) :
q = ↑q.num
source
theorem Rat.den_eq_one_iff (r : ℚ) :
r.den = 1 ↔ ↑r.num = r
source
📐 coverage
instance Rat.canLift :
CanLift ℚ ℤ Int.cast fun (q : ℚ) => q.den = 1
source
theorem Rat.coe_int_inj (m n : ℤ) :
↑m = ↑n ↔ m = n
source
🔸 coverage
def Rat.divCasesOn {C : ℚ → Sort u_1} (a : ℚ) (div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)) :
C a

A version of Rat.casesOn that uses / instead of Rat.mk'. Use as

cases r with
| div p q nonzero coprime =>
Instances For