Mathlib.Data.Rat.Defs

Rat.pos theorem

(a : ℚ) : 0 < a.den

Full source

theorem pos (a : ℚ) : 0 < a.den := Nat.pos_of_ne_zero a.den_nz

Positivity of Denominator in Rational Numbers

Informal description

For any rational number $a$, the denominator of $a$ is strictly positive, i.e., $0 < \text{den}(a)$.

Rat.mk'_num_den theorem

(q : ℚ) : mk' q.num q.den q.den_nz q.reduced = q

Full source

lemma mk'_num_den (q : ℚ) : mk' q.num q.den q.den_nz q.reduced = q := rfl

Canonical Construction of Rational Numbers via Numerator and Denominator

Informal description

For any rational number $q$, the construction `mk'` with numerator $q.\text{num}$, denominator $q.\text{den}$, and proofs that the denominator is nonzero and the fraction is reduced, yields $q$ itself. In other words, $\text{mk'}(q.\text{num}, q.\text{den}, q.\text{den\_nz}, q.\text{reduced}) = q$.

Rat.ofInt_eq_cast theorem

(n : ℤ) : ofInt n = Int.cast n

Full source

@[simp]
theorem ofInt_eq_cast (n : ℤ) : ofInt n = Int.cast n :=
  rfl

Equality of Rational Construction from Integer and Integer Cast

Informal description

For any integer $n$, the rational number constructed from $n$ via `Rat.ofInt` is equal to the canonical embedding of $n$ into the rational numbers via `Int.cast`.

Rat.num_ofNat theorem

(n : ℕ) : num ofNat(n) = ofNat(n)

Full source

@[simp] lemma num_ofNat (n : ℕ) : num ofNat(n) = ofNat(n) := rfl

Numerator of Natural Number as Rational Number

Informal description

For any natural number $n$, the numerator of the rational number constructed from $n$ (via `ofNat`) is equal to $n$ itself.

Rat.den_ofNat theorem

(n : ℕ) : den ofNat(n) = 1

Full source

@[simp] lemma den_ofNat (n : ℕ) : den ofNat(n) = 1 := rfl

Denominator of Natural Number as Rational is One

Informal description

For any natural number $n$, the denominator of the rational number constructed from $n$ is equal to 1.

Rat.num_natCast theorem

(n : ℕ) : num n = n

Full source

@[simp, norm_cast] lemma num_natCast (n : ℕ) : num n = n := rfl

Numerator of Natural Number Cast to Rationals

Informal description

For any natural number $n$, the numerator of the rational number corresponding to $n$ is equal to $n$ itself.

Rat.den_natCast theorem

(n : ℕ) : den n = 1

Full source

@[simp, norm_cast] lemma den_natCast (n : ℕ) : den n = 1 := rfl

Denominator of Natural Number as Rational is One

Informal description

For any natural number $n$, the denominator of the rational number representation of $n$ is equal to $1$.

Rat.num_intCast theorem

(n : ℤ) : (n : ℚ).num = n

Full source

@[simp, norm_cast] lemma num_intCast (n : ℤ) : (n : ℚ).num = n := rfl

Numerator of Integer Cast to Rationals Equals Original Integer

Informal description

For any integer $n$, the numerator of the rational number obtained by casting $n$ to $\mathbb{Q}$ is equal to $n$ itself.

Rat.den_intCast theorem

(n : ℤ) : (n : ℚ).den = 1

Full source

@[simp, norm_cast] lemma den_intCast (n : ℤ) : (n : ℚ).den = 1 := rfl

Denominator of Integer Cast to Rationals is One

Informal description

For any integer $n$, the denominator of the rational number obtained by casting $n$ to $\mathbb{Q}$ is equal to $1$.

Rat.intCast_injective theorem

: Injective (Int.cast : ℤ → ℚ)

Full source

lemma intCast_injective : Injective (Int.cast : ℤ → ℚ) := fun _ _ ↦ congr_arg num

Injectivity of Integer Embedding into Rational Numbers

Informal description

The canonical embedding of the integers into the rational numbers, given by the function $n \mapsto \frac{n}{1}$, is injective. In other words, if $m, n \in \mathbb{Z}$ satisfy $\frac{m}{1} = \frac{n}{1}$ in $\mathbb{Q}$, then $m = n$.

Rat.natCast_injective theorem

: Injective (Nat.cast : ℕ → ℚ)

Full source

lemma natCast_injective : Injective (Nat.cast : ℕ → ℚ) :=
  intCast_injective.comp fun _ _ ↦ Int.natCast_inj.1

Injectivity of Natural Number Embedding into Rational Numbers

Informal description

The canonical embedding of the natural numbers into the rational numbers, given by the function $n \mapsto \frac{n}{1}$, is injective. In other words, if $m, n \in \mathbb{N}$ satisfy $\frac{m}{1} = \frac{n}{1}$ in $\mathbb{Q}$, then $m = n$.

Rat.natCast_inj theorem

{m n : ℕ} : (m : ℚ) = n ↔ m = n

Full source

@[simp high, norm_cast] lemma natCast_inj {m n : ℕ} : (m : ℚ) = n ↔ m = n :=
  natCast_injective.eq_iff

Injectivity of Natural Number Cast to Rational Numbers: $(m : \mathbb{Q}) = (n : \mathbb{Q}) \leftrightarrow m = n$

Informal description

For any natural numbers $m$ and $n$, the equality $(m : \mathbb{Q}) = (n : \mathbb{Q})$ holds if and only if $m = n$.

Rat.intCast_eq_zero theorem

{n : ℤ} : (n : ℚ) = 0 ↔ n = 0

Full source

@[simp high, norm_cast] lemma intCast_eq_zero {n : ℤ} : (n : ℚ) = 0 ↔ n = 0 := intCast_inj

Integer Cast to Rational is Zero iff Integer is Zero

Informal description

For any integer $n$, the rational number obtained by casting $n$ to $\mathbb{Q}$ is equal to zero if and only if $n$ itself is zero, i.e., $(n : \mathbb{Q}) = 0 \leftrightarrow n = 0$.

Rat.natCast_eq_zero theorem

{n : ℕ} : (n : ℚ) = 0 ↔ n = 0

Full source

@[simp high, norm_cast] lemma natCast_eq_zero {n : ℕ} : (n : ℚ) = 0 ↔ n = 0 := natCast_inj

Natural Number Cast to Rational is Zero iff Natural Number is Zero

Informal description

For any natural number $n$, the rational number obtained by casting $n$ to $\mathbb{Q}$ is equal to zero if and only if $n$ itself is zero, i.e., $(n : \mathbb{Q}) = 0 \leftrightarrow n = 0$.

Rat.intCast_eq_one theorem

{n : ℤ} : (n : ℚ) = 1 ↔ n = 1

Full source

@[simp high, norm_cast] lemma intCast_eq_one {n : ℤ} : (n : ℚ) = 1 ↔ n = 1 := intCast_inj

Integer Cast to Rational Equals One if and Only if Integer is One

Informal description

For any integer $n$, the rational number obtained by casting $n$ to $\mathbb{Q}$ is equal to $1$ if and only if $n = 1$.

Rat.natCast_eq_one theorem

{n : ℕ} : (n : ℚ) = 1 ↔ n = 1

Full source

@[simp high, norm_cast] lemma natCast_eq_one {n : ℕ} : (n : ℚ) = 1 ↔ n = 1 := natCast_inj

Natural Number Cast to Rational Equals One if and Only if Natural Number is One

Informal description

For any natural number $n$, the rational number obtained by casting $n$ to $\mathbb{Q}$ is equal to $1$ if and only if $n = 1$.

Rat.mkRat_eq_divInt theorem

(n d) : mkRat n d = n /. d

Full source

lemma mkRat_eq_divInt (n d) : mkRat n d = n /. d := rfl

Equality of Rational Number Constructions: $\text{mkRat}(n, d) = n / d$

Informal description

For any integers $n$ and $d$, the rational number constructed using `mkRat n d` is equal to the rational number $n / d$ constructed using the division notation `/.`.

Rat.mk'_zero theorem

(d) (h : d ≠ 0) (w) : mk' 0 d h w = 0

Full source

@[simp] lemma mk'_zero (d) (h : d ≠ 0) (w) : mk' 0 d h w = 0 := by congr; simp_all

Zero Numerator Yields Zero in Rational Construction

Informal description

For any nonzero integer $d$ and any proof $h$ that $d \neq 0$, the rational number constructed as $\text{mk'}(0, d, h, w)$ is equal to $0$, regardless of the additional argument $w$.

Rat.num_eq_zero theorem

{q : ℚ} : q.num = 0 ↔ q = 0

Full source

@[simp]
lemma num_eq_zero {q : ℚ} : q.num = 0 ↔ q = 0 := by
  induction q
  constructor
  · rintro rfl
    exact mk'_zero _ _ _
  · exact congr_arg num

Zero Numerator Characterizes Zero Rational Number

Informal description

For any rational number $q$, the numerator of $q$ is zero if and only if $q$ is zero, i.e., $q.\text{num} = 0 \leftrightarrow q = 0$.

Rat.num_ne_zero theorem

{q : ℚ} : q.num ≠ 0 ↔ q ≠ 0

Full source

lemma num_ne_zero {q : ℚ} : q.num ≠ 0q.num ≠ 0 ↔ q ≠ 0 := num_eq_zero.not

Nonzero Numerator Characterizes Nonzero Rational Number

Informal description

For any rational number $q$, the numerator of $q$ is nonzero if and only if $q$ itself is nonzero, i.e., $q.\text{num} \neq 0 \leftrightarrow q \neq 0$.

Rat.den_ne_zero theorem

(q : ℚ) : q.den ≠ 0

Full source

@[simp] lemma den_ne_zero (q : ℚ) : q.den ≠ 0 := q.den_pos.ne'

Nonzero Denominator Property of Rational Numbers

Informal description

For any rational number $q$, the denominator of $q$ is nonzero.

Rat.num_nonneg theorem

: 0 ≤ q.num ↔ 0 ≤ q

Full source

@[simp] lemma num_nonneg : 0 ≤ q.num ↔ 0 ≤ q := by
  simp [Int.le_iff_lt_or_eq, instLE, Rat.blt, Int.not_lt]; tauto

Nonnegativity of Rational Number and Its Numerator

Informal description

For any rational number $q$, the numerator of $q$ is nonnegative if and only if $q$ itself is nonnegative.

Rat.divInt_eq_zero theorem

{a b : ℤ} (b0 : b ≠ 0) : a /. b = 0 ↔ a = 0

Full source

@[simp]
theorem divInt_eq_zero {a b : ℤ} (b0 : b ≠ 0) : a /. ba /. b = 0 ↔ a = 0 := by
  rw [← zero_divInt b, divInt_eq_iff b0 b0, Int.zero_mul, Int.mul_eq_zero, or_iff_left b0]

Rational Number Zero Criterion: $\frac{a}{b} = 0 \leftrightarrow a = 0$

Informal description

For any integers $a$ and $b$ with $b \neq 0$, the rational number $\frac{a}{b}$ equals zero if and only if $a = 0$.

Rat.divInt_ne_zero theorem

{a b : ℤ} (b0 : b ≠ 0) : a /. b ≠ 0 ↔ a ≠ 0

Full source

theorem divInt_ne_zero {a b : ℤ} (b0 : b ≠ 0) : a /. ba /. b ≠ 0a /. b ≠ 0 ↔ a ≠ 0 :=
  (divInt_eq_zero b0).not

Nonzero Criterion for Rational Numbers: $\frac{a}{b} \neq 0 \leftrightarrow a \neq 0$

Informal description

For any integers $a$ and $b$ with $b \neq 0$, the rational number $\frac{a}{b}$ is nonzero if and only if $a$ is nonzero.

Rat.normalize_eq_mk' theorem

(n : Int) (d : Nat) (h : d ≠ 0) (c : Nat.gcd (Int.natAbs n) d = 1) : normalize n d h = mk' n d h c

Full source

theorem normalize_eq_mk' (n : Int) (d : Nat) (h : d ≠ 0) (c : Nat.gcd (Int.natAbs n) d = 1) :
    normalize n d h = mk' n d h c := (mk_eq_normalize ..).symm

Normalized Rational Equals Canonical Form When Coprime

Informal description

For integers $n$ and natural numbers $d \neq 0$ with $\gcd(|n|, d) = 1$, the normalized form of the rational number $n/d$ equals the canonical form $\text{mk'}\ n\ d\ h\ c$, where $h$ is the proof that $d \neq 0$ and $c$ is the proof of the coprimality condition.

Rat.num_divInt_den theorem

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

Full source

lemma num_divInt_den (q : ℚ) : q.num /. q.den = q := divInt_self _

Rational Number as Fraction of Its Numerator and Denominator

Informal description

For any rational number $q$, the fraction formed by its numerator and denominator equals $q$ itself, i.e., $\frac{\text{num}(q)}{\text{den}(q)} = q$.

Rat.mk'_eq_divInt theorem

{n d h c} : (⟨n, d, h, c⟩ : ℚ) = n /. d

Full source

lemma mk'_eq_divInt {n d h c} : (⟨n, d, h, c⟩ : ℚ) = n /. d := (num_divInt_den _).symm

Canonical Rational Equals Fraction Representation

Informal description

For any integer $n$, natural number $d \neq 0$ (with proof $h$), and proof $c$ that $\gcd(|n|, d) = 1$, the canonical rational number $\langle n, d, h, c \rangle$ is equal to the fraction $n / d$.

Rat.intCast_eq_divInt theorem

(z : ℤ) : (z : ℚ) = z /. 1

Full source

theorem intCast_eq_divInt (z : ℤ) : (z : ℚ) = z /. 1 := mk'_eq_divInt

Integer Embedding as Rational Fraction with Denominator One

Informal description

For any integer $z$, the canonical embedding of $z$ into the rational numbers is equal to the fraction $z / 1$.

Rat.divInt_self' theorem

{n : ℤ} (hn : n ≠ 0) : n /. n = 1

Full source

@[simp] lemma divInt_self' {n : ℤ} (hn : n ≠ 0) : n /. n = 1 := by
  simpa using divInt_mul_right (n := 1) (d := 1) hn

Self-Division of Nonzero Integer Yields One

Informal description

For any nonzero integer $n$, the rational number formed by dividing $n$ by itself is equal to $1$, i.e., $\frac{n}{n} = 1$.

Rat.numDenCasesOn definition

{C : ℚ → Sort u} : ∀ (a : ℚ) (_ : ∀ n d, 0 < d → (Int.natAbs n).Coprime d → C (n /. d)), C a

Full source

/-- 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`. -/
@[elab_as_elim]
def numDenCasesOn.{u} {C : ℚ → Sort u} :
    ∀ (a : ℚ) (_ : ∀ n d, 0 < d → (Int.natAbs n).Coprime d → C (n /. d)), C a
  | ⟨n, d, h, c⟩, H => by rw [mk'_eq_divInt]; exact H n d (Nat.pos_of_ne_zero h) c

Case analysis for rational numbers in reduced form

Informal description

Given a predicate $C$ on rational numbers and a rational number $a$, to prove $C(a)$ it suffices to consider rational numbers of the form $n / d$ where $d > 0$ and the absolute value of $n$ is coprime with $d$, and show that $C(n / d)$ holds for all such $n$ and $d$.

Rat.numDenCasesOn' definition

{C : ℚ → Sort u} (a : ℚ) (H : ∀ (n : ℤ) (d : ℕ), d ≠ 0 → C (n /. d)) : C a

Full source

/-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with rational
numbers of the form `n /. d` with `d ≠ 0`. -/
@[elab_as_elim]
def numDenCasesOn'.{u} {C : ℚ → Sort u} (a : ℚ) (H : ∀ (n : ℤ) (d : ℕ), d ≠ 0 → C (n /. d)) :
    C a :=
  numDenCasesOn a fun n d h _ => H n d h.ne'

Case analysis for rational numbers in numerator-denominator form

Informal description

Given a predicate $C$ on rational numbers and a rational number $a$, to prove $C(a)$ it suffices to consider rational numbers of the form $n / d$ where $d$ is a nonzero natural number, and show that $C(n / d)$ holds for all such $n$ and $d$.

Rat.numDenCasesOn'' definition

{C : ℚ → Sort u} (a : ℚ) (H : ∀ (n : ℤ) (d : ℕ) (nz red), C (mk' n d nz red)) : C a

Full source

/-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with rational
numbers of the form `mk' n d` with `d ≠ 0`. -/
@[elab_as_elim]
def numDenCasesOn''.{u} {C : ℚ → Sort u} (a : ℚ)
    (H : ∀ (n : ℤ) (d : ℕ) (nz red), C (mk' n d nz red)) : C a :=
  numDenCasesOn a fun n d h h' ↦ by rw [← mk_eq_divInt _ _ h.ne' h']; exact H n d h.ne' _

Case analysis for rational numbers via constructor mk'

Informal description

Given a predicate $C$ on rational numbers and a rational number $a$, to prove $C(a)$ it suffices to consider rational numbers constructed as $\text{mk'}\ n\ d$ with $d \neq 0$ and $\text{Int.natAbs}\ n$ coprime with $d$, and show that $C(\text{mk'}\ n\ d\ \text{nz}\ \text{red})$ holds for all such $n$, $d$, and proofs $\text{nz}$ of $d \neq 0$ and $\text{red}$ of coprimality.

Rat.lift_binop_eq theorem

 (f : ℚ → ℚ → ℚ) (f₁ : ℤ → ℤ → ℤ → ℤ → ℤ) (f₂ : ℤ → ℤ → ℤ → ℤ → ℤ)
  (fv : ∀ {n₁ d₁ h₁ c₁ n₂ d₂ h₂ c₂}, f ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ = 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 (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d

Full source

theorem lift_binop_eq (f : ℚ → ℚ → ℚ) (f₁ : ℤ → ℤ → ℤ → ℤ → ℤ) (f₂ : ℤ → ℤ → ℤ → ℤ → ℤ)
    (fv :
      ∀ {n₁ d₁ h₁ c₁ n₂ d₂ h₂ c₂},
        f ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ = 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 (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d := by
  generalize ha : a /. b = x; obtain ⟨n₁, d₁, h₁, c₁⟩ := x; rw [mk'_eq_divInt] at ha
  generalize hc : c /. d = x; obtain ⟨n₂, d₂, h₂, c₂⟩ := x; rw [mk'_eq_divInt] at hc
  rw [fv]
  have d₁0 := Int.ofNat_ne_zero.2 h₁
  have d₂0 := Int.ofNat_ne_zero.2 h₂
  exact (divInt_eq_iff (f0 d₁0 d₂0) (f0 b0 d0)).2
    (H ((divInt_eq_iff b0 d₁0).1 ha) ((divInt_eq_iff d0 d₂0).1 hc))

Lifting of Binary Operation on Rationals via Integer Functions

Informal description

Let $f : \mathbb{Q} \times \mathbb{Q} \to \mathbb{Q}$ be a binary operation on rational numbers, and let $f_1, f_2 : \mathbb{Z}^4 \to \mathbb{Z}$ be integer-valued functions. Suppose that: 1. For any rational numbers $\langle n_1, d_1, h_1, c_1 \rangle$ and $\langle n_2, d_2, h_2, c_2 \rangle$, we have: $$f\left(\langle n_1, d_1, h_1, c_1 \rangle, \langle n_2, d_2, h_2, c_2 \rangle\right) = \frac{f_1(n_1, d_1, n_2, d_2)}{f_2(n_1, d_1, n_2, d_2)}.$$ 2. For any integers $n_1, d_1, n_2, d_2$ with $d_1 \neq 0$ and $d_2 \neq 0$, we have $f_2(n_1, d_1, n_2, d_2) \neq 0$. 3. For any integers $a, b, c, d$ with $b \neq 0$ and $d \neq 0$, and for any integers $n_1, d_1, n_2, d_2$ satisfying: $$a \cdot d_1 = n_1 \cdot b \quad \text{and} \quad c \cdot d_2 = n_2 \cdot d,$$ we have the compatibility condition: $$f_1(n_1, d_1, n_2, d_2) \cdot f_2(a, b, c, d) = f_1(a, b, c, d) \cdot f_2(n_1, d_1, n_2, d_2).$$ Then, for any integers $a, b, c, d$ with $b \neq 0$ and $d \neq 0$, we have: $$f\left(\frac{a}{b}, \frac{c}{d}\right) = \frac{f_1(a, b, c, d)}{f_2(a, b, c, d)}.$$

Rat.neg_def theorem

(q : ℚ) : -q = -q.num /. q.den

Full source

lemma neg_def (q : ℚ) : -q = -q.num /. q.den := by rw [← neg_divInt, num_divInt_den]

Negation of Rational Number as Fraction of Negated Numerator and Denominator

Informal description

For any rational number $q$, the negation of $q$ is equal to the fraction formed by the negation of its numerator and its denominator, i.e., $-q = \frac{-\text{num}(q)}{\text{den}(q)}$.

Rat.divInt_neg theorem

(n d : ℤ) : n /. -d = -n /. d

Full source

@[simp] lemma divInt_neg (n d : ℤ) : n /. -d = -n /. d := divInt_neg' ..

Negation of Denominator in Rational Number Construction

Informal description

For any integers $n$ and $d$, the rational number $\frac{n}{-d}$ is equal to $\frac{-n}{d}$.

Rat.divInt_mul_divInt' theorem

(n₁ d₁ n₂ d₂ : ℤ) : (n₁ /. d₁) * (n₂ /. d₂) = (n₁ * n₂) /. (d₁ * d₂)

Full source

@[simp]
lemma divInt_mul_divInt' (n₁ d₁ n₂ d₂ : ℤ) : (n₁ /. d₁) * (n₂ /. d₂) = (n₁ * n₂) /. (d₁ * d₂) := by
  obtain rfl | h₁ := eq_or_ne d₁ 0
  · simp
  obtain rfl | h₂ := eq_or_ne d₂ 0
  · simp
  exact divInt_mul_divInt _ _ h₁ h₂

Multiplication Formula for Rational Numbers: $(n_1/d_1) \cdot (n_2/d_2) = (n_1n_2)/(d_1d_2)$

Informal description

For any integers $n_1, d_1, n_2, d_2$, the product of the rational numbers $n_1 / d_1$ and $n_2 / d_2$ is equal to $(n_1 \cdot n_2) / (d_1 \cdot d_2)$.

Rat.mk'_mul_mk' theorem

 (n₁ n₂ : ℤ) (d₁ d₂ : ℕ) (hd₁ hd₂ hnd₁ hnd₂) (h₁₂ : n₁.natAbs.Coprime d₂) (h₂₁ : n₂.natAbs.Coprime d₁) :
  mk' n₁ d₁ hd₁ hnd₁ * mk' n₂ d₂ hd₂ hnd₂ =
    mk' (n₁ * n₂) (d₁ * d₂) (Nat.mul_ne_zero hd₁ hd₂)
      (by rw [Int.natAbs_mul]; exact (hnd₁.mul h₂₁).mul_right (h₁₂.mul hnd₂))

Full source

lemma mk'_mul_mk' (n₁ n₂ : ℤ) (d₁ d₂ : ℕ) (hd₁ hd₂ hnd₁ hnd₂) (h₁₂ : n₁.natAbs.Coprime d₂)
    (h₂₁ : n₂.natAbs.Coprime d₁) :
    mk' n₁ d₁ hd₁ hnd₁ * mk' n₂ d₂ hd₂ hnd₂ = mk' (n₁ * n₂) (d₁ * d₂) (Nat.mul_ne_zero hd₁ hd₂) (by
      rw [Int.natAbs_mul]; exact (hnd₁.mul h₂₁).mul_right (h₁₂.mul hnd₂)) := by
  rw [mul_def]; dsimp; simp [mk_eq_normalize]

Multiplication of Reduced Rational Numbers in Terms of Numerators and Denominators

Informal description

Let $n_1, n_2 \in \mathbb{Z}$ and $d_1, d_2 \in \mathbb{N}$ with $d_1 \neq 0$, $d_2 \neq 0$, $\gcd(|n_1|, d_1) = 1$, and $\gcd(|n_2|, d_2) = 1$. Suppose further that $\gcd(|n_1|, d_2) = 1$ and $\gcd(|n_2|, d_1) = 1$. Then the product of the rational numbers $\frac{n_1}{d_1}$ and $\frac{n_2}{d_2}$ (in reduced form) is equal to $\frac{n_1 n_2}{d_1 d_2}$ (also in reduced form).

Rat.mul_eq_mkRat theorem

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

Full source

lemma mul_eq_mkRat (q r : ℚ) : q * r = mkRat (q.num * r.num) (q.den * r.den) := by
  rw [mul_def, normalize_eq_mkRat]

Product of Rational Numbers as Reduced Fraction of Numerator and Denominator Products

Informal description

For any rational numbers $q$ and $r$, their product $q \cdot r$ is equal to the reduced form of the rational number with numerator $q_\text{num} \cdot r_\text{num}$ and denominator $q_\text{den} \cdot r_\text{den}$, where $q_\text{num}$ and $r_\text{num}$ are the numerators of $q$ and $r$ respectively, and $q_\text{den}$ and $r_\text{den}$ are their denominators.

Rat.instPowNat instance

: Pow ℚ ℕ

Full source

instance instPowNat : Pow ℚ ℕ where
  pow q n := ⟨q.num ^ n, q.den ^ n, by simp [Nat.pow_eq_zero], by
    rw [Int.natAbs_pow]; exact q.reduced.pow _ _⟩

Natural Power Operation on Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ can be equipped with a natural power operation $q^n$ for $q \in \mathbb{Q}$ and $n \in \mathbb{N}$, defined by raising the numerator and denominator to the power $n$ separately.

Rat.pow_def theorem

 (q : ℚ) (n : ℕ) :
  q ^ n = ⟨q.num ^ n, q.den ^ n, by simp [Nat.pow_eq_zero], by rw [Int.natAbs_pow]; exact q.reduced.pow _ _⟩

Full source

lemma pow_def (q : ℚ) (n : ℕ) :
    q ^ n = ⟨q.num ^ n, q.den ^ n,
      by simp [Nat.pow_eq_zero],
      by rw [Int.natAbs_pow]; exact q.reduced.pow _ _⟩ := rfl

Definition of Rational Number Exponentiation via Numerator and Denominator Powers

Informal description

For any rational number $q$ and natural number $n$, the power $q^n$ is equal to the rational number with numerator $q_\text{num}^n$ and denominator $q_\text{den}^n$, where $q_\text{num}$ and $q_\text{den}$ are the numerator and denominator of $q$ in reduced form. Moreover, this construction preserves the reduced form property of the rational number.

Rat.pow_eq_mkRat theorem

(q : ℚ) (n : ℕ) : q ^ n = mkRat (q.num ^ n) (q.den ^ n)

Full source

lemma pow_eq_mkRat (q : ℚ) (n : ℕ) : q ^ n = mkRat (q.num ^ n) (q.den ^ n) := by
  rw [pow_def, mk_eq_mkRat]

Rational Power as Reduced Fraction of Powers

Informal description

For any rational number $q$ and natural number $n$, the power $q^n$ is equal to the rational number constructed from the numerator $q_\text{num}^n$ and denominator $q_\text{den}^n$ in reduced form.

Rat.pow_eq_divInt theorem

(q : ℚ) (n : ℕ) : q ^ n = q.num ^ n /. q.den ^ n

Full source

lemma pow_eq_divInt (q : ℚ) (n : ℕ) : q ^ n = q.num ^ n /. q.den ^ n := by
  rw [pow_def, mk_eq_divInt, Int.natCast_pow]

Rational Power as Fraction of Powers: $q^n = \frac{q_{\text{num}}^n}{q_{\text{den}}^n}$

Informal description

For any rational number $q$ and natural number $n$, the power $q^n$ is equal to the fraction $\frac{q_{\text{num}}^n}{q_{\text{den}}^n}$, where $q_{\text{num}}$ and $q_{\text{den}}$ are the numerator and denominator of $q$ respectively.

Rat.num_pow theorem

(q : ℚ) (n : ℕ) : (q ^ n).num = q.num ^ n

Full source

@[simp] lemma num_pow (q : ℚ) (n : ℕ) : (q ^ n).num = q.num ^ n := rfl

Numerator of Rational Power Equals Power of Numerator

Informal description

For any rational number $q$ and natural number $n$, the numerator of $q^n$ is equal to the $n$-th power of the numerator of $q$, i.e., $(q^n)_{\text{num}} = (q_{\text{num}})^n$.

Rat.den_pow theorem

(q : ℚ) (n : ℕ) : (q ^ n).den = q.den ^ n

Full source

@[simp] lemma den_pow (q : ℚ) (n : ℕ) : (q ^ n).den = q.den ^ n := rfl

Denominator of Rational Power Equals Power of Denominator

Informal description

For any rational number $q$ and natural number $n$, the denominator of $q^n$ is equal to the $n$-th power of the denominator of $q$, i.e., $\text{den}(q^n) = (\text{den}(q))^n$.

Rat.mk'_pow theorem

 (num : ℤ) (den : ℕ) (hd hdn) (n : ℕ) :
  mk' num den hd hdn ^ n =
    mk' (num ^ n) (den ^ n) (by simp [Nat.pow_eq_zero, hd]) (by rw [Int.natAbs_pow]; exact hdn.pow _ _)

Full source

@[simp] lemma mk'_pow (num : ℤ) (den : ℕ) (hd hdn) (n : ℕ) :
    mk' num den hd hdn ^ n = mk' (num ^ n) (den ^ n)
      (by simp [Nat.pow_eq_zero, hd]) (by rw [Int.natAbs_pow]; exact hdn.pow _ _) := rfl

Power of Rational Number in Reduced Form: $\left(\frac{num}{den}\right)^n = \frac{num^n}{den^n}$

Informal description

For integers $num$ and $den$ (with $den \neq 0$ and $den$ not dividing $num$), and a natural number $n$, the $n$-th power of the rational number $\frac{num}{den}$ is equal to the rational number $\frac{num^n}{den^n}$.

Rat.instInv instance

: Inv ℚ

Full source

instance : Inv ℚ :=
  ⟨Rat.inv⟩

Inversion Operation on Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ have an inversion operation, where for any rational number $q = n/d$ with $n, d \in \mathbb{Z}$ and $d \neq 0$, the inverse $q^{-1}$ is given by $d/n$.

Rat.inv_divInt' theorem

(a b : ℤ) : (a /. b)⁻¹ = b /. a

Full source

@[simp] lemma inv_divInt' (a b : ℤ) : (a /. b)⁻¹ = b /. a := inv_divInt ..

Inverse of Rational Number as Fraction of Integers: $(a / b)^{-1} = b / a$

Informal description

For any integers $a$ and $b$, the inverse of the rational number $a / b$ is equal to $b / a$.

Rat.inv_mkRat theorem

(a : ℤ) (b : ℕ) : (mkRat a b)⁻¹ = b /. a

Full source

@[simp] lemma inv_mkRat (a : ℤ) (b : ℕ) : (mkRat a b)⁻¹ = b /. a := by
  rw [mkRat_eq_divInt, inv_divInt']

Inverse of Rational Construction: $(\text{mkRat}(a, b))^{-1} = b / a$

Informal description

For any integer $a$ and natural number $b$, the inverse of the rational number $\text{mkRat}(a, b)$ is equal to $b / a$.

Rat.inv_def' theorem

(q : ℚ) : q⁻¹ = q.den /. q.num

Full source

lemma inv_def' (q : ℚ) : q⁻¹ = q.den /. q.num := by rw [← inv_divInt', num_divInt_den]

Inverse of Rational Number as Denominator over Numerator: $q^{-1} = \text{den}(q)/\text{num}(q)$

Informal description

For any rational number $q$, the inverse $q^{-1}$ is equal to the fraction formed by its denominator over its numerator, i.e., $q^{-1} = \frac{\text{den}(q)}{\text{num}(q)}$.

Rat.divInt_div_divInt theorem

(n₁ d₁ n₂ d₂) : (n₁ /. d₁) / (n₂ /. d₂) = (n₁ * d₂) /. (d₁ * n₂)

Full source

@[simp] lemma divInt_div_divInt (n₁ d₁ n₂ d₂) :
    (n₁ /. d₁) / (n₂ /. d₂) = (n₁ * d₂) /. (d₁ * n₂) := by
  rw [div_def, inv_divInt, divInt_mul_divInt']

Division Formula for Rational Numbers: $(n_1/d_1) / (n_2/d_2) = (n_1d_2)/(d_1n_2)$

Informal description

For any integers $n_1, d_1, n_2, d_2$, the division of the rational numbers $n_1 / d_1$ by $n_2 / d_2$ is equal to $(n_1 \cdot d_2) / (d_1 \cdot n_2)$.

Rat.div_def' theorem

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

Full source

lemma div_def' (q r : ℚ) : q / r = (q.num * r.den) /. (q.den * r.num) := by
  rw [← divInt_div_divInt, num_divInt_den, num_divInt_den]

Division of Rational Numbers in Terms of Numerator and Denominator

Informal description

For any rational numbers $q$ and $r$, the division $q / r$ is equal to the fraction formed by the product of $q$'s numerator and $r$'s denominator over the product of $q$'s denominator and $r$'s numerator, i.e., $q / r = \frac{\text{num}(q) \cdot \text{den}(r)}{\text{den}(q) \cdot \text{num}(r)}$.

Rat.add_zero theorem

: a + 0 = a

Full source

protected lemma add_zero : a + 0 = a := by simp [add_def, normalize_eq_mkRat]

Right Additive Identity for Rational Numbers

Informal description

For any rational number $a$, the sum $a + 0$ equals $a$.

Rat.zero_add theorem

: 0 + a = a

Full source

protected lemma zero_add : 0 + a = a := by simp [add_def, normalize_eq_mkRat]

Additive Identity Property for Rational Numbers

Informal description

For any rational number $a$, the sum of $0$ and $a$ is equal to $a$, i.e., $0 + a = a$.

Rat.add_comm theorem

: a + b = b + a

Full source

protected lemma add_comm : a + b = b + a := by
  simp [add_def, Int.add_comm, Int.mul_comm, Nat.mul_comm]

Commutativity of Addition for Rational Numbers

Informal description

For any rational numbers $a$ and $b$, the sum $a + b$ is equal to $b + a$.

Rat.add_assoc theorem

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

Full source

protected theorem add_assoc : a + b + c = a + (b + c) :=
  numDenCasesOn' a fun n₁ d₁ h₁ ↦ numDenCasesOn' b fun n₂ d₂ h₂ ↦ numDenCasesOn' c fun n₃ d₃ h₃ ↦ by
    simp only [ne_eq, Int.natCast_eq_zero, h₁, not_false_eq_true, h₂, divInt_add_divInt,
      Int.mul_eq_zero, or_self, h₃]
    rw [Int.mul_assoc, Int.add_mul, Int.add_mul, Int.mul_assoc, Int.add_assoc]
    congr 2
    ac_rfl

Associativity of Addition for Rational Numbers

Informal description

For any rational numbers $a$, $b$, and $c$, the sum $(a + b) + c$ is equal to $a + (b + c)$.

Rat.neg_add_cancel theorem

: -a + a = 0

Full source

protected lemma neg_add_cancel : -a + a = 0 := by
  simp [add_def, normalize_eq_mkRat, Int.neg_mul, Int.add_comm, ← Int.sub_eq_add_neg]

Additive Inverse Property for Rational Numbers

Informal description

For any rational number $a$, the sum of $-a$ and $a$ equals $0$, i.e., $-a + a = 0$.

Rat.divInt_one theorem

(n : ℤ) : n /. 1 = n

Full source

@[simp] lemma divInt_one (n : ℤ) : n /. 1 = n := by simp [divInt, mkRat, normalize]

Division by One in Rational Numbers: $n / 1 = n$

Informal description

For any integer $n$, the rational number $n / 1$ is equal to $n$.

Rat.mkRat_one theorem

(n : ℤ) : mkRat n 1 = n

Full source

@[simp] lemma mkRat_one (n : ℤ) : mkRat n 1 = n := by simp [mkRat_eq_divInt]

Rational Construction with Denominator One: $\mathrm{mkRat}(n, 1) = n$

Informal description

For any integer $n$, the rational number constructed as $\mathrm{mkRat}(n, 1)$ is equal to $n$.

Rat.divInt_one_one theorem

: 1 /. 1 = 1

Full source

lemma divInt_one_one : 1 /. 1 = 1 := by rw [divInt_one, intCast_one]

Division of One by One in Rational Numbers: $1 / 1 = 1$

Informal description

The rational number $1 / 1$ is equal to $1$.

Rat.mul_assoc theorem

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

Full source

protected theorem mul_assoc : a * b * c = a * (b * c) :=
  numDenCasesOn' a fun n₁ d₁ h₁ =>
    numDenCasesOn' b fun n₂ d₂ h₂ =>
      numDenCasesOn' c fun n₃ d₃ h₃ => by
        simp [h₁, h₂, h₃, Int.mul_comm, Nat.mul_assoc, Int.mul_left_comm]

Associativity of Multiplication in Rational Numbers: $(a \cdot b) \cdot c = a \cdot (b \cdot c)$

Informal description

For any rational numbers $a$, $b$, and $c$, the multiplication operation is associative, i.e., $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.

Rat.add_mul theorem

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

Full source

protected theorem add_mul : (a + b) * c = a * c + b * c :=
  numDenCasesOn' a fun n₁ d₁ h₁ ↦ numDenCasesOn' b fun n₂ d₂ h₂ ↦ numDenCasesOn' c fun n₃ d₃ h₃ ↦ by
    simp only [ne_eq, Int.natCast_eq_zero, h₁, not_false_eq_true, h₂, divInt_add_divInt,
      Int.mul_eq_zero, or_self, h₃, divInt_mul_divInt]
    rw [← divInt_mul_right (Int.natCast_ne_zero.2 h₃), Int.add_mul, Int.add_mul]
    ac_rfl

Right Distributivity of Multiplication over Addition in Rational Numbers: $(a + b)c = ac + bc$

Informal description

For any rational numbers $a$, $b$, and $c$, the following distributive property holds: $$(a + b) \cdot c = a \cdot c + b \cdot c.$$

Rat.mul_add theorem

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

Full source

protected theorem mul_add : a * (b + c) = a * b + a * c := by
  rw [Rat.mul_comm, Rat.add_mul, Rat.mul_comm, Rat.mul_comm c a]

Left Distributivity of Multiplication over Addition in Rational Numbers: $a(b + c) = ab + ac$

Informal description

For any rational numbers $a$, $b$, and $c$, the following distributive property holds: $$a \cdot (b + c) = a \cdot b + a \cdot c.$$

Rat.zero_ne_one theorem

: 0 ≠ (1 : ℚ)

Full source

protected theorem zero_ne_one : 0 ≠ (1 : ℚ) := by
  rw [ne_comm, ← divInt_one_one, divInt_ne_zero] <;> omega

Non-Equality of Zero and One in Rational Numbers: $0 \neq 1$

Informal description

The rational number $0$ is not equal to $1$, i.e., $0 \neq 1$ in $\mathbb{Q}$.

Rat.mul_inv_cancel theorem

: a ≠ 0 → a * a⁻¹ = 1

Full source

protected theorem mul_inv_cancel : a ≠ 0 → a * a⁻¹ = 1 :=
  numDenCasesOn' a fun n d hd hn ↦ by
    simp only [divInt_ofNat, ne_eq, hd, not_false_eq_true, mkRat_eq_zero] at hn
    simp [-divInt_ofNat, mkRat_eq_divInt, Int.mul_comm, Int.mul_ne_zero hn (Int.ofNat_ne_zero.2 hd)]

Multiplicative Inverse Property for Rational Numbers: $a \cdot a^{-1} = 1$ when $a \neq 0$

Informal description

For any nonzero rational number $a$, the product of $a$ and its multiplicative inverse $a^{-1}$ equals $1$, i.e., $a \cdot a^{-1} = 1$.

Rat.inv_mul_cancel theorem

(h : a ≠ 0) : a⁻¹ * a = 1

Full source

protected theorem inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 :=
  Eq.trans (Rat.mul_comm _ _) (Rat.mul_inv_cancel _ h)

Inverse Multiplication Identity for Rational Numbers: $a^{-1} \cdot a = 1$ when $a \neq 0$

Informal description

For any nonzero rational number $a$, the product of its multiplicative inverse $a^{-1}$ and $a$ equals $1$, i.e., $a^{-1} \cdot a = 1$.

Rat.nontrivial instance

: Nontrivial ℚ

Full source

instance nontrivial : Nontrivial ℚ where exists_pair_ne := ⟨1, 0, by decide⟩

Nontriviality of the Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ form a nontrivial type, meaning there exist distinct elements in $\mathbb{Q}$.

Rat.addCommGroup instance

: AddCommGroup ℚ

Full source

instance addCommGroup : AddCommGroup ℚ where
  zero := 0
  add := (· + ·)
  neg := Neg.neg
  zero_add := Rat.zero_add
  add_zero := Rat.add_zero
  add_comm := Rat.add_comm
  add_assoc := Rat.add_assoc
  neg_add_cancel := Rat.neg_add_cancel
  sub_eq_add_neg := Rat.sub_eq_add_neg
  nsmul := nsmulRec
  zsmul := zsmulRec

Rational Numbers as an Additive Commutative Group

Informal description

The rational numbers $\mathbb{Q}$ form an additive commutative group.

Rat.addGroup instance

: AddGroup ℚ

Full source

instance addGroup : AddGroup ℚ := by infer_instance

Rational Numbers as an Additive Group

Informal description

The rational numbers $\mathbb{Q}$ form an additive group.

Rat.addCommMonoid instance

: AddCommMonoid ℚ

Full source

instance addCommMonoid : AddCommMonoid ℚ := by infer_instance

Rational Numbers as an Additive Commutative Monoid

Informal description

The rational numbers $\mathbb{Q}$ form an additive commutative monoid.

Rat.addMonoid instance

: AddMonoid ℚ

Full source

instance addMonoid : AddMonoid ℚ := by infer_instance

Rational Numbers as an Additive Monoid

Informal description

The rational numbers $\mathbb{Q}$ form an additive monoid.

Rat.addLeftCancelSemigroup instance

: AddLeftCancelSemigroup ℚ

Full source

instance addLeftCancelSemigroup : AddLeftCancelSemigroup ℚ := by infer_instance

Rational Numbers as an Additive Left Cancellative Semigroup

Informal description

The rational numbers $\mathbb{Q}$ form an additive left cancellative semigroup.

Rat.addRightCancelSemigroup instance

: AddRightCancelSemigroup ℚ

Full source

instance addRightCancelSemigroup : AddRightCancelSemigroup ℚ := by infer_instance

Rational Numbers as an Additive Right Cancellative Semigroup

Informal description

The rational numbers $\mathbb{Q}$ form an additive right cancellative semigroup.

Rat.addCommSemigroup instance

: AddCommSemigroup ℚ

Full source

instance addCommSemigroup : AddCommSemigroup ℚ := by infer_instance

Rational Numbers as an Additive Commutative Semigroup

Informal description

The rational numbers $\mathbb{Q}$ form an additive commutative semigroup.

Rat.addSemigroup instance

: AddSemigroup ℚ

Full source

instance addSemigroup : AddSemigroup ℚ := by infer_instance

Rational Numbers as an Additive Semigroup

Informal description

The rational numbers $\mathbb{Q}$ form an additive semigroup.

Rat.commMonoid instance

: CommMonoid ℚ

Full source

instance commMonoid : CommMonoid ℚ where
  one := 1
  mul := (· * ·)
  mul_one := Rat.mul_one
  one_mul := Rat.one_mul
  mul_comm := Rat.mul_comm
  mul_assoc := Rat.mul_assoc
  npow n q := q ^ n
  npow_zero := by intros; apply Rat.ext <;> simp [Int.pow_zero]
  npow_succ n q := by
    rw [← q.mk'_num_den, mk'_pow, mk'_mul_mk']
    · congr
    · rw [mk'_pow, Int.natAbs_pow]
      exact q.reduced.pow_left _
    · rw [mk'_pow]
      exact q.reduced.pow_right _

Rational Numbers as a Commutative Monoid

Informal description

The rational numbers $\mathbb{Q}$ form a commutative monoid under multiplication.

Rat.monoid instance

: Monoid ℚ

Full source

instance monoid : Monoid ℚ := by infer_instance

Rational Numbers as a Monoid

Informal description

The rational numbers $\mathbb{Q}$ form a monoid under multiplication.

Rat.commSemigroup instance

: CommSemigroup ℚ

Full source

instance commSemigroup : CommSemigroup ℚ := by infer_instance

Rational Numbers as a Commutative Semigroup

Informal description

The rational numbers $\mathbb{Q}$ form a commutative semigroup under multiplication.

Rat.semigroup instance

: Semigroup ℚ

Full source

instance semigroup : Semigroup ℚ := by infer_instance

Rational Numbers as a Semigroup

Informal description

The rational numbers $\mathbb{Q}$ form a semigroup under multiplication.

Rat.den_neg_eq_den theorem

(q : ℚ) : (-q).den = q.den

Full source

@[simp]
theorem den_neg_eq_den (q : ℚ) : (-q).den = q.den :=
  rfl

Denominator is Preserved Under Negation in Rational Numbers

Informal description

For any rational number $q$, the denominator of $-q$ is equal to the denominator of $q$.

Rat.num_neg_eq_neg_num theorem

(q : ℚ) : (-q).num = -q.num

Full source

@[simp]
theorem num_neg_eq_neg_num (q : ℚ) : (-q).num = -q.num :=
  rfl

Negation Preserves Numerator in Rational Numbers

Informal description

For any rational number $q$, the numerator of $-q$ is equal to the negation of the numerator of $q$, i.e., $\text{num}(-q) = -\text{num}(q)$.

Rat.num_zero theorem

: Rat.num 0 = 0

Full source

theorem num_zero : Rat.num 0 = 0 :=
  rfl

Numerator of Zero is Zero

Informal description

The numerator of the rational number $0$ is equal to $0$, i.e., $\text{num}(0) = 0$.

Rat.den_zero theorem

: Rat.den 0 = 1

Full source

theorem den_zero : Rat.den 0 = 1 :=
  rfl

Denominator of Zero is One

Informal description

The denominator of the rational number $0$ is $1$, i.e., $\text{den}(0) = 1$.

Rat.zero_of_num_zero theorem

{q : ℚ} (hq : q.num = 0) : q = 0

Full source

lemma zero_of_num_zero {q : ℚ} (hq : q.num = 0) : q = 0 := by simpa [hq] using q.num_divInt_den.symm

Zero Rational Number from Zero Numerator

Informal description

For any rational number $q$, if the numerator of $q$ is zero, then $q$ is equal to zero, i.e., $\text{num}(q) = 0 \implies q = 0$.

Rat.zero_iff_num_zero theorem

{q : ℚ} : q = 0 ↔ q.num = 0

Full source

theorem zero_iff_num_zero {q : ℚ} : q = 0 ↔ q.num = 0 :=
  ⟨fun _ => by simp [*], zero_of_num_zero⟩

Zero Rational Number Characterization via Numerator

Informal description

For any rational number $q$, $q = 0$ if and only if the numerator of $q$ is zero, i.e., $q = 0 \leftrightarrow \text{num}(q) = 0$.

Rat.num_one theorem

: (1 : ℚ).num = 1

Full source

theorem num_one : (1 : ℚ).num = 1 :=
  rfl

Numerator of One Equals One

Informal description

The numerator of the rational number $1$ is equal to $1$, i.e., $\text{num}(1) = 1$.

Rat.den_one theorem

: (1 : ℚ).den = 1

Full source

@[simp]
theorem den_one : (1 : ℚ).den = 1 :=
  rfl

Denominator of One is One

Informal description

The denominator of the rational number $1$ is equal to $1$.

Rat.mk_num_ne_zero_of_ne_zero theorem

{q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : n ≠ 0

Full source

theorem mk_num_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : n ≠ 0 :=
  fun this => hq <| by simpa [this] using hqnd

Nonzero rational implies nonzero numerator

Informal description

For any nonzero rational number $q = n / d$ (where $n, d \in \mathbb{Z}$), the numerator $n$ is nonzero.

Rat.mk_denom_ne_zero_of_ne_zero theorem

{q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : d ≠ 0

Full source

theorem mk_denom_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = n /. d) : d ≠ 0 :=
  fun this => hq <| by simpa [this] using hqnd

Nonzero Rational Implies Nonzero Denominator

Informal description

For any nonzero rational number $q = n / d$ where $n, d \in \mathbb{Z}$, the denominator $d$ is nonzero.

Rat.divInt_ne_zero_of_ne_zero theorem

{n d : ℤ} (h : n ≠ 0) (hd : d ≠ 0) : n /. d ≠ 0

Full source

theorem divInt_ne_zero_of_ne_zero {n d : ℤ} (h : n ≠ 0) (hd : d ≠ 0) : n /. dn /. d ≠ 0 :=
  (divInt_ne_zero hd).mpr h

Nonzero Rational from Nonzero Integers: $\frac{n}{d} \neq 0$

Informal description

For any integers $n$ and $d$ with $n \neq 0$ and $d \neq 0$, the rational number $\frac{n}{d}$ is nonzero.

Rat.nonneg_antisymm theorem

: 0 ≤ q → 0 ≤ -q → q = 0

Full source

protected lemma nonneg_antisymm : 0 ≤ q → 0 ≤ -q → q = 0 := by
  simp_rw [← num_eq_zero, Int.le_antisymm_iff, ← num_nonneg, num_neg_eq_neg_num, Int.neg_nonneg]
  tauto

Antisymmetry of Nonnegativity for Rational Numbers

Informal description

For any rational number $q$, if $0 \leq q$ and $0 \leq -q$, then $q = 0$.

Rat.nonneg_total theorem

(a : ℚ) : 0 ≤ a ∨ 0 ≤ -a

Full source

protected lemma nonneg_total (a : ℚ) : 0 ≤ a ∨ 0 ≤ -a := by
  simp_rw [← num_nonneg, num_neg_eq_neg_num, Int.neg_nonneg]; exact Int.le_total _ _

Total Non-Negativity for Rational Numbers

Informal description

For any rational number $a$, either $a$ is non-negative or $-a$ is non-negative, i.e., $0 \leq a \lor 0 \leq -a$.

Rat.add_divInt theorem

(a b c : ℤ) : (a + b) /. c = a /. c + b /. c

Full source

protected theorem add_divInt (a b c : ℤ) : (a + b) /. c = a /. c + b /. c :=
  if h : c = 0 then by simp [h]
  else by
    rw [divInt_add_divInt _ _ h h, divInt_eq_iff h (Int.mul_ne_zero h h)]
    simp [Int.add_mul, Int.mul_assoc]

Additivity of Rational Division: $(a + b)/c = a/c + b/c$ for integers $a,b,c$

Informal description

For any integers $a$, $b$, and $c$, the rational number $(a + b) \mkern1mu /. \mkern1mu c$ is equal to the sum of the rational numbers $a \mkern1mu /. \mkern1mu c$ and $b \mkern1mu /. \mkern1mu c$, i.e., $(a + b) \mkern1mu /. \mkern1mu c = (a \mkern1mu /. \mkern1mu c) + (b \mkern1mu /. \mkern1mu c)$.

Rat.divInt_eq_div theorem

(n d : ℤ) : n /. d = (n : ℚ) / d

Full source

theorem divInt_eq_div (n d : ℤ) : n /. d = (n : ℚ) / d := by simp [div_def']

Equivalence of Division Notation and Rational Division: $n \mkern1mu /. \mkern1mu d = \frac{n}{d}$

Informal description

For any integers $n$ and $d$, the rational number constructed by the division operation `n /. d` is equal to the quotient of the rational number obtained by coercing $n$ to $\mathbb{Q}$ divided by $d$, i.e., $n \mkern1mu /. \mkern1mu d = \frac{n}{d}$.

Rat.intCast_div_eq_divInt theorem

(n d : ℤ) : (n : ℚ) / (d) = n /. d

Full source

lemma intCast_div_eq_divInt (n d : ℤ) : (n : ℚ) / (d) = n /. d := by rw [divInt_eq_div]

Rational Division Equivalence: $\frac{n}{d} = n \mkern1mu /. \mkern1mu d$ for integers $n,d$

Informal description

For any integers $n$ and $d$, the division of the rational number obtained by coercing $n$ to $\mathbb{Q}$ by $d$ equals the rational number constructed by the division operation `n /. d`, i.e., $\frac{n}{d} = n \mkern1mu /. \mkern1mu d$.

Rat.natCast_div_eq_divInt theorem

(n d : ℕ) : (n : ℚ) / d = n /. d

Full source

theorem natCast_div_eq_divInt (n d : ℕ) : (n : ℚ) / d = n /. d := Rat.intCast_div_eq_divInt n d

Rational Division Equivalence for Natural Numbers: $\frac{n}{d} = n \mkern1mu /. \mkern1mu d$

Informal description

For any natural numbers $n$ and $d$, the division of the rational number obtained by coercing $n$ to $\mathbb{Q}$ by $d$ equals the rational number constructed by the division operation `n /. d`, i.e., $\frac{n}{d} = n \mkern1mu /. \mkern1mu d$.

Rat.divInt_mul_divInt_cancel theorem

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

Full source

theorem divInt_mul_divInt_cancel {x : ℤ} (hx : x ≠ 0) (n d : ℤ) : n /. x * (x /. d) = n /. d := by
  by_cases hd : d = 0
  · rw [hd]
    simp
  rw [divInt_mul_divInt _ _ hx hd, x.mul_comm, divInt_mul_right hx]

Cancellation of Rational Multiplication: $\frac{n}{x} \cdot \frac{x}{d} = \frac{n}{d}$ for $x \neq 0$

Informal description

For any integers $x \neq 0$, $n$, and $d$, the product of the rational numbers $\frac{n}{x}$ and $\frac{x}{d}$ equals $\frac{n}{d}$.

Rat.coe_int_num_of_den_eq_one theorem

{q : ℚ} (hq : q.den = 1) : (q.num : ℚ) = q

Full source

theorem coe_int_num_of_den_eq_one {q : ℚ} (hq : q.den = 1) : (q.num : ℚ) = q := by
  conv_rhs => rw [← num_divInt_den q, hq]
  rw [intCast_eq_divInt]
  rfl

Rational Number with Unit Denominator is Integer Embedding

Informal description

For any rational number $q$ with denominator equal to 1, the canonical embedding of its numerator into the rational numbers equals $q$ itself, i.e., $\text{num}(q) = q$.

Rat.den_eq_one_iff theorem

(r : ℚ) : r.den = 1 ↔ ↑r.num = r

Full source

theorem den_eq_one_iff (r : ℚ) : r.den = 1 ↔ ↑r.num = r :=
  ⟨Rat.coe_int_num_of_den_eq_one, fun h => h ▸ Rat.den_intCast r.num⟩

Characterization of Rational Numbers with Unit Denominator

Informal description

For any rational number $r$, the denominator of $r$ equals $1$ if and only if the canonical embedding of its numerator into the rational numbers equals $r$ itself, i.e., $r.\text{den} = 1 \leftrightarrow \text{num}(r) = r$.

Rat.canLift instance

: CanLift ℚ ℤ (↑) fun q => q.den = 1

Full source

instance canLift : CanLift ℚ ℤ (↑) fun q => q.den = 1 :=
  ⟨fun q hq => ⟨q.num, coe_int_num_of_den_eq_one hq⟩⟩

Lifting Integers to Rational Numbers with Unit Denominator

Informal description

There exists a canonical way to lift an integer to a rational number with denominator 1.

Rat.coe_int_inj theorem

(m n : ℤ) : (m : ℚ) = n ↔ m = n

Full source

theorem coe_int_inj (m n : ℤ) : (m : ℚ) = n ↔ m = n :=
  ⟨congr_arg num, congr_arg _⟩

Injectivity of Integer to Rational Number Canonical Map

Informal description

For any integers $m$ and $n$, the canonical injection from $\mathbb{Z}$ to $\mathbb{Q}$ maps $m$ and $n$ to the same rational number if and only if $m = n$.

Rat.divCasesOn definition

{C : ℚ → Sort*} (a : ℚ) (div : ∀ (n : ℤ) (d : ℕ), d ≠ 0 → n.natAbs.Coprime d → C (n / d)) : C a

Full source

/--
A version of `Rat.casesOn` that uses `/` instead of `Rat.mk'`. Use as
```lean
cases r with
| div p q nonzero coprime =>
```
-/
@[elab_as_elim, cases_eliminator, induction_eliminator]
def divCasesOn {C : ℚ → Sort*} (a : ℚ)
    (div : ∀ (n : ℤ) (d : ℕ), d ≠ 0 → n.natAbs.Coprime d → C (n / d)) : C a :=
  a.casesOn fun n d nz red => by rw [Rat.mk'_eq_divInt, Rat.divInt_eq_div]; exact div n d nz red

Case analysis on rational numbers via numerator-denominator form

Informal description

Given a rational number $ a $ and a function `div` that takes an integer $ n $, a natural number $ d $, a proof that $ d \neq 0 $, and a proof that the absolute value of $ n $ is coprime with $ d $, and returns a term of type $ C(n / d) $, the function `Rat.divCasesOn` constructs a term of type $ C(a) $ by decomposing $ a $ into the form $ n / d $ with the given properties.

Mathlib.Data.Rat.Defs

Summary

Main Definitions

Notations