Mathlib.Algebra.Ring.Rat

Module docstring

{"# The rational numbers are a commutative ring

This file contains the commutative ring instance on the rational numbers.

See note [foundational algebra order theory]. ","### Instances ","### Extra instances to short-circuit type class resolution

These also prevent non-computable instances being used to construct these instances non-computably. ","### Miscellaneous lemmas "}

Rat.commRing instance

: CommRing ℚ

Full source

instance commRing : CommRing ℚ where
  __ := addCommGroup
  __ := commMonoid
  zero_mul := Rat.zero_mul
  mul_zero := Rat.mul_zero
  left_distrib := Rat.mul_add
  right_distrib := Rat.add_mul
  intCast := fun n => n
  natCast n := Int.cast n
  natCast_zero := rfl
  natCast_succ n := by
    simp only [intCast_eq_divInt, divInt_add_divInt _ _ Int.one_ne_zero Int.one_ne_zero,
      ← divInt_one_one, Int.natCast_add, Int.natCast_one, mul_one]

The Rational Numbers as a Commutative Ring

Informal description

The rational numbers $\mathbb{Q}$ form a commutative ring.

Rat.commGroupWithZero instance

: CommGroupWithZero ℚ

Full source

instance commGroupWithZero : CommGroupWithZero ℚ :=
  { exists_pair_ne := ⟨0, 1, Rat.zero_ne_one⟩
    inv_zero := by
      change Rat.inv 0 = 0
      rw [Rat.inv_def]
      rfl
    mul_inv_cancel := Rat.mul_inv_cancel
    mul_zero := mul_zero
    zero_mul := zero_mul }

Rational Numbers as a Commutative Group with Zero

Informal description

The rational numbers $\mathbb{Q}$ form a commutative group with zero, where every nonzero element has a multiplicative inverse and multiplication is commutative.

Rat.isDomain instance

: IsDomain ℚ

Full source

instance isDomain : IsDomain ℚ := NoZeroDivisors.to_isDomain _

Rational Numbers Form a Domain

Informal description

The rational numbers $\mathbb{Q}$ form a domain, meaning they are a nontrivial commutative ring where multiplication by any nonzero element is cancellative on both sides.

Rat.instCharZero instance

: CharZero ℚ

Full source

/-- The characteristic of `ℚ` is 0. -/
@[stacks 09FS "Second part."]
instance instCharZero : CharZero ℚ where cast_injective a b hab := by simpa using congr_arg num hab

Characteristic Zero Property of Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ have characteristic zero, meaning the canonical map from the natural numbers to $\mathbb{Q}$ is injective.

Rat.commSemiring instance

: CommSemiring ℚ

Full source

instance commSemiring : CommSemiring ℚ := by infer_instance

The Commutative Semiring Structure on Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ form a commutative semiring.

Rat.semiring instance

: Semiring ℚ

Full source

instance semiring : Semiring ℚ := by infer_instance

The Semiring Structure on Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ form a semiring.

Rat.mkRat_eq_div theorem

(n : ℤ) (d : ℕ) : mkRat n d = n / d

Full source

lemma mkRat_eq_div (n : ℤ) (d : ℕ) : mkRat n d = n / d := by
  simp only [mkRat_eq_divInt, divInt_eq_div, Int.cast_natCast]

Equality of Rational Construction and Division: $\text{mkRat}(n, d) = \frac{n}{d}$

Informal description

For any integer $n$ and natural number $d$, the rational number constructed as `mkRat n d` equals the division of $n$ by $d$ in the rational numbers, i.e., $\text{mkRat}(n, d) = \frac{n}{d}$.

Rat.divInt_div_divInt_cancel_left theorem

{x : ℤ} (hx : x ≠ 0) (n d : ℤ) : n /. x / (d /. x) = n /. d

Full source

lemma divInt_div_divInt_cancel_left {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :
    n /. x / (d /. x) = n /. d := by
  rw [div_eq_mul_inv, inv_divInt', divInt_mul_divInt_cancel hx]

Cancellation of Division in Rationals: $\frac{n/x}{d/x} = \frac{n}{d}$ for $x \neq 0$

Informal description

For any nonzero integer $x$ and integers $n, d$, the division of the rational numbers $\frac{n}{x}$ by $\frac{d}{x}$ equals $\frac{n}{d}$.

Rat.divInt_div_divInt_cancel_right theorem

{x : ℤ} (hx : x ≠ 0) (n d : ℤ) : x /. n / (x /. d) = d /. n

Full source

lemma divInt_div_divInt_cancel_right {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :
    x /. n / (x /. d) = d /. n := by
  rw [div_eq_mul_inv, inv_divInt', mul_comm, divInt_mul_divInt_cancel hx]

Right Cancellation of Division in Rationals: $\frac{x/n}{x/d} = d/n$ for $x \neq 0$

Informal description

For any nonzero integer $x$ and integers $n, d$, the division of the rational numbers $\frac{x}{n}$ by $\frac{x}{d}$ equals $\frac{d}{n}$.

Rat.num_div_den theorem

(r : ℚ) : (r.num : ℚ) / (r.den : ℚ) = r

Full source

lemma num_div_den (r : ℚ) : (r.num : ℚ) / (r.den : ℚ) = r := by
  rw [← Int.cast_natCast, ← divInt_eq_div, num_divInt_den]

Rational Number as Quotient of Numerator and Denominator

Informal description

For any rational number $r$, the quotient of its numerator and denominator (both interpreted as rational numbers) equals $r$ itself, i.e., $\frac{\text{num}(r)}{\text{den}(r)} = r$.

Rat.divInt_pow theorem

(num : ℕ) (den : ℤ) (n : ℕ) : (num /. den) ^ n = num ^ n /. den ^ n

Full source

@[simp] lemma divInt_pow (num : ℕ) (den : ℤ) (n : ℕ) : (num /. den) ^ n = num ^ n /. den ^ n := by
  simp [divInt_eq_div, div_pow, Int.natCast_pow]

Power of Rational Number as Fraction of Powers: $(num /. den)^n = num^n /. den^n$

Informal description

For any natural number `num`, integer `den`, and natural number `n`, the `n`-th power of the rational number `num /. den` is equal to the rational number `num^n /. den^n`.

Rat.mkRat_pow theorem

(num den : ℕ) (n : ℕ) : mkRat num den ^ n = mkRat (num ^ n) (den ^ n)

Full source

@[simp] lemma mkRat_pow (num den : ℕ) (n : ℕ) : mkRat num den ^ n = mkRat (num ^ n) (den ^ n) := by
  rw [mkRat_eq_divInt, mkRat_eq_divInt, divInt_pow, Int.natCast_pow]

Power of Rational Number Construction: $\text{mkRat}(num, den)^n = \text{mkRat}(num^n, den^n)$

Informal description

For any natural numbers $num$, $den$, and $n$, the $n$-th power of the rational number $\text{mkRat}(num, den)$ is equal to $\text{mkRat}(num^n, den^n)$.

Rat.natCast_eq_divInt theorem

(n : ℕ) : ↑n = n /. 1

Full source

lemma natCast_eq_divInt (n : ℕ) : ↑n = n /. 1 := by rw [← Int.cast_natCast, intCast_eq_divInt]

Natural Number Embedding as Rational Fraction with Denominator One

Informal description

For any natural number $n$, the canonical embedding of $n$ into the rational numbers is equal to the fraction $n / 1$.

Rat.mul_den_eq_num theorem

(q : ℚ) : q * q.den = q.num

Full source

@[simp] lemma mul_den_eq_num (q : ℚ) : q * q.den = q.num := by
  suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by
    conv => pattern (occs := 1) q; (rw [← num_divInt_den q])
    simp only [intCast_eq_divInt, natCast_eq_divInt, num_divInt_den] at this ⊢; assumption
  have : (q.den : ℤ) ≠ 0 := mod_cast q.den_ne_zero
  rw [divInt_mul_divInt _ _ this Int.one_ne_zero, mul_comm (q.den : ℤ) 1, divInt_mul_right this]

Rational Number Property: $q \cdot \text{den}(q) = \text{num}(q)$

Informal description

For any rational number $q$, multiplying $q$ by its denominator $\text{den}(q)$ yields its numerator $\text{num}(q)$, i.e., $q \cdot \text{den}(q) = \text{num}(q)$.

Rat.den_mul_eq_num theorem

(q : ℚ) : q.den * q = q.num

Full source

@[simp] lemma den_mul_eq_num (q : ℚ) : q.den * q = q.num := by rw [mul_comm, mul_den_eq_num]

Rational Number Property: Denominator Multiplied by Number Equals Numerator

Informal description

For any rational number $q$, multiplying its denominator $\text{den}(q)$ by $q$ yields its numerator $\text{num}(q)$, i.e., $\text{den}(q) \cdot q = \text{num}(q)$.