Mathlib.Data.Rat.Lemmas

Rat.num_dvd theorem

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

Full source

theorem num_dvd (a) {b : ℤ} (b0 : b ≠ 0) : (a /. b).num ∣ a := by
  rcases e : a /. b with ⟨n, d, h, c⟩
  rw [Rat.mk'_eq_divInt, divInt_eq_iff b0 (mod_cast h)] at e
  refine Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <|
    c.dvd_of_dvd_mul_right ?_
  have := congr_arg Int.natAbs e
  simp only [Int.natAbs_mul, Int.natAbs_natCast] at this; simp [this]

Numerator of Reduced Fraction Divides Original Numerator

Informal description

For any integer $a$ and nonzero integer $b$, the numerator of the reduced fraction $a / b$ divides $a$.

Rat.den_dvd theorem

(a b : ℤ) : ((a /. b).den : ℤ) ∣ b

Full source

theorem den_dvd (a b : ℤ) : ((a /. b).den : ℤ) ∣ b := by
  by_cases b0 : b = 0; · simp [b0]
  rcases e : a /. b with ⟨n, d, h, c⟩
  rw [mk'_eq_divInt, divInt_eq_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e
  refine Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.symm.dvd_of_dvd_mul_left ?_
  rw [← Int.natAbs_mul, ← Int.natCast_dvd_natCast, Int.dvd_natAbs, ← e]; simp

Denominator of Reduced Fraction Divides Original Denominator

Informal description

For any integers $a$ and $b$, the denominator of the reduced fraction $a / b$ (viewed as an integer) divides $b$.

Rat.num_den_mk theorem

{q : ℚ} {n d : ℤ} (hd : d ≠ 0) (qdf : q = n /. d) : ∃ c : ℤ, n = c * q.num ∧ d = c * q.den

Full source

theorem num_den_mk {q : ℚ} {n d : ℤ} (hd : d ≠ 0) (qdf : q = n /. d) :
    ∃ c : ℤ, n = c * q.num ∧ d = c * q.den := by
  obtain rfl | hn := eq_or_ne n 0
  · simp [qdf]
  have : q.num * d = n * ↑q.den := by
    refine (divInt_eq_iff ?_ hd).mp ?_
    · exact Int.natCast_ne_zero.mpr (Rat.den_nz _)
    · rwa [num_divInt_den]
  have hqdn : q.num ∣ n := by
    rw [qdf]
    exact Rat.num_dvd _ hd
  refine ⟨n / q.num, ?_, ?_⟩
  · rw [Int.ediv_mul_cancel hqdn]
  · refine Int.eq_mul_div_of_mul_eq_mul_of_dvd_left ?_ hqdn this
    rw [qdf]
    exact Rat.num_ne_zero.2 ((divInt_ne_zero hd).mpr hn)

Factorization of Numerator and Denominator in Reduced Rational Form

Informal description

For any rational number $q$ and integers $n$ and $d$ with $d \neq 0$, if $q = \frac{n}{d}$, then there exists an integer $c$ such that $n = c \cdot \text{num}(q)$ and $d = c \cdot \text{den}(q)$, where $\text{num}(q)$ and $\text{den}(q)$ are the numerator and denominator of $q$ in reduced form.

Rat.num_mk theorem

(n d : ℤ) : (n /. d).num = d.sign * n / n.gcd d

Full source

theorem num_mk (n d : ℤ) : (n /. d).num = d.sign * n / n.gcd d := by
  have (m : ℕ) : Int.natAbs (m + 1) = m + 1 := by
    rw [← Nat.cast_one, ← Nat.cast_add, Int.natAbs_cast]
  rcases d with ((_ | _) | _) <;>
  rw [← Int.tdiv_eq_ediv_of_dvd] <;>
  simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd,
    Int.zero_ediv, Int.ofNat_dvd_left, Nat.gcd_dvd_left, this]

Numerator Formula for Reduced Rational Number Construction

Informal description

For any integers $n$ and $d$, the numerator of the rational number $n/d$ (in reduced form) is equal to $\text{sign}(d) \cdot n$ divided by the greatest common divisor of $n$ and $d$.

Rat.den_mk theorem

(n d : ℤ) : (n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d

Full source

theorem den_mk (n d : ℤ) : (n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d := by
  have (m : ℕ) : Int.natAbs (m + 1) = m + 1 := by
    rw [← Nat.cast_one, ← Nat.cast_add, Int.natAbs_cast]
  rcases d with ((_ | _) | _) <;>
    simp [divInt, mkRat, Rat.normalize, Nat.succPNat, Int.sign, Int.gcd,
      if_neg (Nat.cast_add_one_ne_zero _), this]

Denominator Formula for Reduced Rational Number Construction

Informal description

For any integers $n$ and $d$, the denominator of the reduced rational number $n/d$ is given by: \[ \text{den}(n/d) = \begin{cases} 1 & \text{if } d = 0, \\ |d| / \gcd(n,d) & \text{otherwise.} \end{cases} \]

Rat.add_den_dvd_lcm theorem

(q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den.lcm q₂.den

Full source

theorem add_den_dvd_lcm (q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den.lcm q₂.den := by
  rw [add_def, normalize_eq, Nat.div_dvd_iff_dvd_mul (Nat.gcd_dvd_right _ _)
    (Nat.gcd_ne_zero_right (by simp)), ← Nat.gcd_mul_lcm,
    mul_dvd_mul_iff_right (Nat.lcm_ne_zero (by simp) (by simp)), Nat.dvd_gcd_iff]
  refine ⟨?_, dvd_mul_right _ _⟩
  rw [← Int.natCast_dvd_natCast, Int.dvd_natAbs]
  apply Int.dvd_add
    <;> apply dvd_mul_of_dvd_right <;> rw [Int.natCast_dvd_natCast]
    <;> [exact Nat.gcd_dvd_right _ _; exact Nat.gcd_dvd_left _ _]

Denominator of Sum Divides LCM of Denominators

Informal description

For any two rational numbers $q_1$ and $q_2$, the denominator of their sum $q_1 + q_2$ divides the least common multiple of the denominators of $q_1$ and $q_2$.

Rat.add_den_dvd theorem

(q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den * q₂.den

Full source

theorem add_den_dvd (q₁ q₂ : ℚ) : (q₁ + q₂).den ∣ q₁.den * q₂.den := by
  rw [add_def, normalize_eq]
  apply Nat.div_dvd_of_dvd
  apply Nat.gcd_dvd_right

Denominator of Sum Divides Product of Denominators

Informal description

For any two rational numbers $q_1$ and $q_2$, the denominator of their sum divides the product of their denominators, i.e., $\text{den}(q_1 + q_2) \mid \text{den}(q_1) \cdot \text{den}(q_2)$.

Rat.mul_den_dvd theorem

(q₁ q₂ : ℚ) : (q₁ * q₂).den ∣ q₁.den * q₂.den

Full source

theorem mul_den_dvd (q₁ q₂ : ℚ) : (q₁ * q₂).den ∣ q₁.den * q₂.den := by
  rw [mul_def, normalize_eq]
  apply Nat.div_dvd_of_dvd
  apply Nat.gcd_dvd_right

Denominator of Product Divides Product of Denominators for Rational Numbers

Informal description

For any two rational numbers $q_1$ and $q_2$, the denominator of their product $q_1 \cdot q_2$ divides the product of their denominators $q_1.\text{den} \cdot q_2.\text{den}$.

Rat.mul_num theorem

 (q₁ q₂ : ℚ) : (q₁ * q₂).num = q₁.num * q₂.num / Nat.gcd (q₁.num * q₂.num).natAbs (q₁.den * q₂.den)

Full source

theorem mul_num (q₁ q₂ : ℚ) :
    (q₁ * q₂).num = q₁.num * q₂.num / Nat.gcd (q₁.num * q₂.num).natAbs (q₁.den * q₂.den) := by
  rw [mul_def, normalize_eq]

Numerator of Product of Rational Numbers

Informal description

For any two rational numbers $q_1$ and $q_2$, the numerator of their product is given by $$(q_1 \cdot q_2)_\text{num} = \frac{(q_1)_\text{num} \cdot (q_2)_\text{num}}{\gcd(|(q_1)_\text{num} \cdot (q_2)_\text{num}|, (q_1)_\text{den} \cdot (q_2)_\text{den})}$$ where $(q)_\text{num}$ and $(q)_\text{den}$ denote the numerator and denominator of $q$ respectively, and $\gcd$ is the greatest common divisor function.

Rat.mul_den theorem

 (q₁ q₂ : ℚ) : (q₁ * q₂).den = q₁.den * q₂.den / Nat.gcd (q₁.num * q₂.num).natAbs (q₁.den * q₂.den)

Full source

theorem mul_den (q₁ q₂ : ℚ) :
    (q₁ * q₂).den =
      q₁.den * q₂.den / Nat.gcd (q₁.num * q₂.num).natAbs (q₁.den * q₂.den) := by
  rw [mul_def, normalize_eq]

Denominator of Product of Rational Numbers

Informal description

For any two rational numbers $q_1$ and $q_2$, the denominator of their product is given by $$(q_1 \cdot q_2).\text{den} = \frac{q_1.\text{den} \cdot q_2.\text{den}}{\gcd(|q_1.\text{num} \cdot q_2.\text{num}|, q_1.\text{den} \cdot q_2.\text{den})},$$ where $\text{num}$ and $\text{den}$ denote the numerator and denominator respectively, and $\gcd$ is the greatest common divisor function.

Rat.mul_self_num theorem

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

Full source

theorem mul_self_num (q : ℚ) : (q * q).num = q.num * q.num := by
  rw [mul_num, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]
  exact (q.reduced.mul_right q.reduced).mul (q.reduced.mul_right q.reduced)

Square of Rational Number's Numerator Equals Numerator of Square

Informal description

For any rational number $q$, the numerator of $q^2$ is equal to the square of the numerator of $q$, i.e., $(q \cdot q)_\text{num} = (q_\text{num})^2$.

Rat.mul_self_den theorem

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

Full source

theorem mul_self_den (q : ℚ) : (q * q).den = q.den * q.den := by
  rw [Rat.mul_den, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Nat.div_one]
  exact (q.reduced.mul_right q.reduced).mul (q.reduced.mul_right q.reduced)

Denominator of Squared Rational Number is Square of Denominator

Informal description

For any rational number $q$, the denominator of its square is equal to the square of its denominator, i.e., $(q \cdot q).\text{den} = q.\text{den} \cdot q.\text{den}$.

Rat.add_num_den theorem

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

Full source

theorem add_num_den (q r : ℚ) :
    q + r = (q.num * r.den + q.den * r.num : ℤ) /. (↑q.den * ↑r.den : ℤ) := by
  have hqd : (q.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 q.den_pos
  have hrd : (r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 r.den_pos
  conv_lhs => rw [← num_divInt_den q, ← num_divInt_den r, divInt_add_divInt _ _ hqd hrd]
  rw [mul_comm r.num q.den]

Addition Formula for Rational Numbers in Terms of Numerators and Denominators

Informal description

For any two rational numbers $q$ and $r$, their sum can be expressed as: \[ q + r = \frac{\text{num}(q) \cdot \text{den}(r) + \text{den}(q) \cdot \text{num}(r)}{\text{den}(q) \cdot \text{den}(r)} \] where $\text{num}(q)$ and $\text{den}(q)$ denote the numerator and denominator of $q$ respectively (and similarly for $r$), and the denominators are cast to integers for the multiplication.

Rat.isSquare_iff theorem

{q : ℚ} : IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den

Full source

theorem isSquare_iff {q : ℚ} : IsSquareIsSquare q ↔ IsSquare q.num ∧ IsSquare q.den := by
  constructor
  · rintro ⟨qr, rfl⟩
    rw [Rat.mul_self_num, mul_self_den]
    simp only [IsSquare.mul_self, and_self]
  · rintro ⟨⟨nr, hnr⟩, ⟨dr, hdr⟩⟩
    refine ⟨nr / dr, ?_⟩
    rw [div_mul_div_comm, ← Int.cast_mul, ← Nat.cast_mul, ← hnr, ← hdr, num_div_den]

Squareness of Rational Number in Terms of Numerator and Denominator

Informal description

A rational number $q$ is a square if and only if both its numerator $\text{num}(q)$ and its denominator $\text{den}(q)$ are squares.

Rat.isSquare_natCast_iff theorem

{n : ℕ} : IsSquare (n : ℚ) ↔ IsSquare n

Full source

@[norm_cast, simp]
theorem isSquare_natCast_iff {n : ℕ} : IsSquareIsSquare (n : ℚ) ↔ IsSquare n := by
  simp_rw [isSquare_iff, num_natCast, den_natCast, IsSquare.one, and_true, Int.isSquare_natCast_iff]

Squareness Preservation in Rational Embedding of Natural Numbers

Informal description

For any natural number $n$, the rational number $n$ (viewed as an element of $\mathbb{Q}$) is a square if and only if $n$ is a square in $\mathbb{N}$.

Rat.isSquare_intCast_iff theorem

{z : ℤ} : IsSquare (z : ℚ) ↔ IsSquare z

Full source

@[norm_cast, simp]
theorem isSquare_intCast_iff {z : ℤ} : IsSquareIsSquare (z : ℚ) ↔ IsSquare z := by
  simp_rw [isSquare_iff, intCast_num, intCast_den, IsSquare.one, and_true]

Square Preservation under Integer to Rational Casting

Informal description

For any integer $z$, the rational number obtained by casting $z$ to $\mathbb{Q}$ is a square if and only if $z$ itself is a square in $\mathbb{Z}$.

Rat.isSquare_ofNat_iff theorem

{n : ℕ} : IsSquare (ofNat(n) : ℚ) ↔ IsSquare (OfNat.ofNat n : ℕ)

Full source

@[simp]
theorem isSquare_ofNat_iff {n : ℕ} :
    IsSquareIsSquare (ofNat(n) : ℚ) ↔ IsSquare (OfNat.ofNat n : ℕ) :=
  isSquare_natCast_iff

Squareness Preservation in Rational Embedding of Natural Numbers via `ofNat`

Informal description

For any natural number $n$, the rational number obtained from the natural number $n$ is a square if and only if $n$ is a square in $\mathbb{N}$.

Rat.exists_eq_mul_div_num_and_eq_mul_div_den theorem

 (n : ℤ) {d : ℤ} (d_ne_zero : d ≠ 0) : ∃ c : ℤ, n = c * ((n : ℚ) / d).num ∧ (d : ℤ) = c * ((n : ℚ) / d).den

Full source

theorem exists_eq_mul_div_num_and_eq_mul_div_den (n : ℤ) {d : ℤ} (d_ne_zero : d ≠ 0) :
    ∃ c : ℤ, n = c * ((n : ℚ) / d).num ∧ (d : ℤ) = c * ((n : ℚ) / d).den :=
  haveI : (n : ℚ) / d = Rat.divInt n d := by rw [← Rat.divInt_eq_div]
  Rat.num_den_mk d_ne_zero this

Factorization of Numerator and Denominator in Rational Division

Informal description

For any integer $n$ and any nonzero integer $d$, there exists an integer $c$ such that: 1. $n = c \cdot \text{num}\left(\frac{n}{d}\right)$, and 2. $d = c \cdot \text{den}\left(\frac{n}{d}\right)$, where $\text{num}(q)$ and $\text{den}(q)$ denote the numerator and denominator (in reduced form) of the rational number $q$.

Rat.mul_num_den' theorem

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

Full source

theorem mul_num_den' (q r : ℚ) :
    (q * r).num * q.den * r.den = q.num * r.num * (q * r).den := by
  let s := q.num * r.num /. (q.den * r.den : ℤ)
  have hs : (q.den * r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.mpr (Nat.mul_pos q.pos r.pos)
  obtain ⟨c, ⟨c_mul_num, c_mul_den⟩⟩ :=
    exists_eq_mul_div_num_and_eq_mul_div_den (q.num * r.num) hs
  rw [c_mul_num, mul_assoc, mul_comm]
  nth_rw 1 [c_mul_den]
  rw [Int.mul_assoc, Int.mul_assoc, mul_eq_mul_left_iff, or_iff_not_imp_right]
  intro
  have h : _ = s := divInt_mul_divInt q.num r.num (mod_cast q.den_ne_zero) (mod_cast r.den_ne_zero)
  rw [num_divInt_den, num_divInt_den] at h
  rw [h, mul_comm, ← Rat.eq_iff_mul_eq_mul, ← divInt_eq_div]

Numerator-Denominator Relation for Multiplication of Rational Numbers

Informal description

For any two rational numbers $q$ and $r$, the product of the numerator of $q \cdot r$ with the denominators of $q$ and $r$ equals the product of the numerators of $q$ and $r$ with the denominator of $q \cdot r$, i.e., $$ \text{num}(q \cdot r) \cdot \text{den}(q) \cdot \text{den}(r) = \text{num}(q) \cdot \text{num}(r) \cdot \text{den}(q \cdot r). $$

Rat.add_num_den' theorem

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

Full source

theorem add_num_den' (q r : ℚ) :
    (q + r).num * q.den * r.den = (q.num * r.den + r.num * q.den) * (q + r).den := by
  let s := divInt (q.num * r.den + r.num * q.den) (q.den * r.den : ℤ)
  have hs : (q.den * r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.mpr (Nat.mul_pos q.pos r.pos)
  obtain ⟨c, ⟨c_mul_num, c_mul_den⟩⟩ :=
    exists_eq_mul_div_num_and_eq_mul_div_den (q.num * r.den + r.num * q.den) hs
  rw [c_mul_num, mul_assoc, mul_comm]
  nth_rw 1 [c_mul_den]
  repeat rw [Int.mul_assoc]
  apply mul_eq_mul_left_iff.2
  rw [or_iff_not_imp_right]
  intro
  have h : _ = s := divInt_add_divInt q.num r.num (mod_cast q.den_ne_zero) (mod_cast r.den_ne_zero)
  rw [num_divInt_den, num_divInt_den] at h
  rw [h]
  rw [mul_comm]
  apply Rat.eq_iff_mul_eq_mul.mp
  rw [← divInt_eq_div]

Numerator-Denominator Relation for Sum of Rational Numbers

Informal description

For any two rational numbers $q$ and $r$, the numerator of their sum multiplied by the denominators of $q$ and $r$ equals the sum of the products of their numerators and denominators, multiplied by the denominator of their sum. That is: $$ \text{num}(q + r) \cdot \text{den}(q) \cdot \text{den}(r) = (\text{num}(q) \cdot \text{den}(r) + \text{num}(r) \cdot \text{den}(q)) \cdot \text{den}(q + r) $$

Rat.substr_num_den' theorem

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

Full source

theorem substr_num_den' (q r : ℚ) :
    (q - r).num * q.den * r.den = (q.num * r.den - r.num * q.den) * (q - r).den := by
  rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r,
    add_num_den' q (-r)]

Numerator-Denominator Relation for Difference of Rational Numbers

Informal description

For any two rational numbers $q$ and $r$, the numerator of their difference multiplied by the denominators of $q$ and $r$ equals the difference of the products of their numerators and denominators, multiplied by the denominator of their difference. That is: $$ \text{num}(q - r) \cdot \text{den}(q) \cdot \text{den}(r) = (\text{num}(q) \cdot \text{den}(r) - \text{num}(r) \cdot \text{den}(q)) \cdot \text{den}(q - r) $$

Rat.inv_neg theorem

(q : ℚ) : (-q)⁻¹ = -q⁻¹

Full source

protected theorem inv_neg (q : ℚ) : (-q)⁻¹ = -q⁻¹ := by
  rw [← num_divInt_den q]
  simp only [Rat.neg_divInt, Rat.inv_divInt', eq_self_iff_true, Rat.divInt_neg]

Inverse of Negative Rational Number: $(-q)^{-1} = -q^{-1}$

Informal description

For any rational number $q$, the inverse of $-q$ is equal to the negation of the inverse of $q$, i.e., $(-q)^{-1} = -q^{-1}$.

Rat.num_div_eq_of_coprime theorem

{a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAbs b.natAbs) : (a / b : ℚ).num = a

Full source

theorem num_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAbs b.natAbs) :
    (a / b : ℚ).num = a := by
  lift b to ℕ using hb0.le
  simp only [Int.natAbs_natCast, Int.ofNat_pos] at h hb0
  rw [← Rat.divInt_eq_div, ← mk_eq_divInt _ _ hb0.ne' h]

Numerator of Reduced Fraction Equals Numerator When Coprime

Informal description

For integers $a$ and $b$ with $b > 0$, if $a$ and $b$ are coprime (i.e., $\gcd(|a|, b) = 1$), then the numerator of the reduced fraction $\frac{a}{b}$ equals $a$.

Rat.den_div_eq_of_coprime theorem

{a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAbs b.natAbs) : ((a / b : ℚ).den : ℤ) = b

Full source

theorem den_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAbs b.natAbs) :
    ((a / b : ℚ).den : ℤ) = b := by
  lift b to ℕ using hb0.le
  simp only [Int.natAbs_natCast, Int.ofNat_pos] at h hb0
  rw [← Rat.divInt_eq_div, ← mk_eq_divInt _ _ hb0.ne' h]

Denominator of Reduced Fraction Equals Denominator When Coprime

Informal description

For integers $a$ and $b$ with $b > 0$, if $a$ and $b$ are coprime (i.e., $\gcd(|a|, b) = 1$), then the denominator of the rational number $\frac{a}{b}$ (when viewed as a reduced fraction) equals $b$.

Rat.div_int_inj theorem

 {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.Coprime a.natAbs b.natAbs) (h2 : Nat.Coprime c.natAbs d.natAbs)
  (h : (a : ℚ) / b = (c : ℚ) / d) : a = c ∧ b = d

Full source

theorem div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.Coprime a.natAbs b.natAbs)
    (h2 : Nat.Coprime c.natAbs d.natAbs) (h : (a : ℚ) / b = (c : ℚ) / d) : a = c ∧ b = d := by
  apply And.intro
  · rw [← num_div_eq_of_coprime hb0 h1, h, num_div_eq_of_coprime hd0 h2]
  · rw [← den_div_eq_of_coprime hb0 h1, h, den_div_eq_of_coprime hd0 h2]

Injective Property of Reduced Fraction Representation in Rational Numbers

Informal description

For integers $a, b, c, d$ with $b > 0$ and $d > 0$, if $\gcd(|a|, b) = 1$ and $\gcd(|c|, d) = 1$, and $\frac{a}{b} = \frac{c}{d}$ as rational numbers, then $a = c$ and $b = d$.

Rat.intCast_div_self theorem

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

Full source

@[norm_cast]
theorem intCast_div_self (n : ℤ) : ((n / n : ℤ) : ℚ) = n / n := by
  by_cases hn : n = 0
  · subst hn
    simp only [Int.cast_zero, Int.zero_tdiv, zero_div, Int.ediv_zero]
  · have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn
    simp only [Int.ediv_self hn, Int.cast_one, Ne, not_false_iff, div_self this]

Canonical Map Preserves Division of Integer by Itself

Informal description

For any integer $n$, the canonical map from $\mathbb{Z}$ to $\mathbb{Q}$ satisfies $\left(\frac{n}{n}\right) = \frac{n}{n}$ in $\mathbb{Q}$.

Rat.natCast_div_self theorem

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

Full source

@[norm_cast]
theorem natCast_div_self (n : ℕ) : ((n / n : ℕ) : ℚ) = n / n :=
  intCast_div_self n

Canonical Map Preserves Division of Natural Number by Itself

Informal description

For any natural number $n$, the canonical map from $\mathbb{N}$ to $\mathbb{Q}$ satisfies $\left(\frac{n}{n}\right) = \frac{n}{n}$ in $\mathbb{Q}$.

Rat.intCast_div theorem

(a b : ℤ) (h : b ∣ a) : ((a / b : ℤ) : ℚ) = a / b

Full source

theorem intCast_div (a b : ℤ) (h : b ∣ a) : ((a / b : ℤ) : ℚ) = a / b := by
  rcases h with ⟨c, rfl⟩
  rw [mul_comm b, Int.mul_ediv_assoc c (dvd_refl b), Int.cast_mul,
    intCast_div_self, Int.cast_mul, mul_div_assoc]

Canonical Map Preserves Division of Integer by Divisor

Informal description

For any integers $a$ and $b$ with $b \neq 0$ and $b$ divides $a$, the canonical map from $\mathbb{Z}$ to $\mathbb{Q}$ satisfies $\left(\frac{a}{b}\right) = \frac{a}{b}$ in $\mathbb{Q}$.

Rat.natCast_div theorem

(a b : ℕ) (h : b ∣ a) : ((a / b : ℕ) : ℚ) = a / b

Full source

theorem natCast_div (a b : ℕ) (h : b ∣ a) : ((a / b : ℕ) : ℚ) = a / b :=
  intCast_div a b (Int.ofNat_dvd.mpr h)

Canonical Map Preserves Division of Natural Number by Divisor

Informal description

For any natural numbers $a$ and $b$ with $b \neq 0$ and $b$ divides $a$, the canonical map from $\mathbb{N}$ to $\mathbb{Q}$ satisfies $\left(\frac{a}{b}\right) = \frac{a}{b}$ in $\mathbb{Q}$.

Rat.den_div_intCast_eq_one_iff theorem

(m n : ℤ) (hn : n ≠ 0) : ((m : ℚ) / n).den = 1 ↔ n ∣ m

Full source

theorem den_div_intCast_eq_one_iff (m n : ℤ) (hn : n ≠ 0) : ((m : ℚ) / n).den = 1 ↔ n ∣ m := by
  replace hn : (n : ℚ) ≠ 0 := num_ne_zero.mp hn
  constructor
  · rw [Rat.den_eq_one_iff, eq_div_iff hn]
    exact mod_cast (Dvd.intro_left _)
  · exact (intCast_div _ _ · ▸ rfl)

Unit Denominator Condition for Rational Division by Integer

Informal description

For any integers $m$ and $n$ with $n \neq 0$, the denominator of the rational number $\frac{m}{n}$ equals $1$ if and only if $n$ divides $m$.

Rat.den_div_natCast_eq_one_iff theorem

(m n : ℕ) (hn : n ≠ 0) : ((m : ℚ) / n).den = 1 ↔ n ∣ m

Full source

theorem den_div_natCast_eq_one_iff (m n : ℕ) (hn : n ≠ 0) : ((m : ℚ) / n).den = 1 ↔ n ∣ m :=
  (den_div_intCast_eq_one_iff m n (Int.ofNat_ne_zero.mpr hn)).trans Int.ofNat_dvd

Unit Denominator Condition for Rational Division by Natural Number

Informal description

For any natural numbers $m$ and $n$ with $n \neq 0$, the denominator of the rational number $\frac{m}{n}$ equals $1$ if and only if $n$ divides $m$.

Rat.inv_intCast_num_of_pos theorem

{a : ℤ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1

Full source

theorem inv_intCast_num_of_pos {a : ℤ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 := by
  rw [← ofInt_eq_cast, ofInt, mk_eq_divInt, Rat.inv_divInt', divInt_eq_div, Nat.cast_one]
  apply num_div_eq_of_coprime ha0
  rw [Int.natAbs_one]
  exact Nat.coprime_one_left _

Numerator of Inverse of Positive Integer in Rationals is One

Informal description

For any positive integer $a$, the numerator of the inverse of the rational number $a$ (viewed as a rational number via the canonical embedding) is equal to $1$.

Rat.inv_natCast_num_of_pos theorem

{a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1

Full source

theorem inv_natCast_num_of_pos {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 :=
  inv_intCast_num_of_pos (mod_cast ha0 : 0 < (a : ℤ))

Numerator of Inverse of Positive Natural Number Cast to Rationals is One

Informal description

For any positive natural number $a$, the numerator of the inverse of the rational number obtained by casting $a$ to $\mathbb{Q}$ is equal to $1$, i.e., $\text{num}(\frac{1}{a}) = 1$.

Rat.inv_intCast_den_of_pos theorem

{a : ℤ} (ha0 : 0 < a) : ((a : ℚ)⁻¹.den : ℤ) = a

Full source

theorem inv_intCast_den_of_pos {a : ℤ} (ha0 : 0 < a) : ((a : ℚ)⁻¹.den : ℤ) = a := by
  rw [← ofInt_eq_cast, ofInt, mk_eq_divInt, Rat.inv_divInt', divInt_eq_div, Nat.cast_one]
  apply den_div_eq_of_coprime ha0
  rw [Int.natAbs_one]
  exact Nat.coprime_one_left _

Denominator of Inverse of Positive Integer Cast to Rationals

Informal description

For any positive integer $a$, the denominator of the inverse of the rational number obtained by casting $a$ to $\mathbb{Q}$ is equal to $a$ itself, i.e., $\text{den}(\frac{1}{a}) = a$.

Rat.inv_natCast_den_of_pos theorem

{a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.den = a

Full source

theorem inv_natCast_den_of_pos {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.den = a := by
  rw [← Int.ofNat_inj, ← Int.cast_natCast a, inv_intCast_den_of_pos]
  rwa [Int.natCast_pos]

Denominator of Inverse of Positive Natural Number Cast to Rationals Equals Original Number

Informal description

For any positive natural number $a$, the denominator of the inverse of the rational number obtained by casting $a$ to $\mathbb{Q}$ is equal to $a$ itself, i.e., $\text{den}(\frac{1}{a}) = a$.

Rat.inv_intCast_num theorem

(a : ℤ) : (a : ℚ)⁻¹.num = Int.sign a

Full source

@[simp]
theorem inv_intCast_num (a : ℤ) : (a : ℚ)⁻¹.num = Int.sign a := by
  rcases lt_trichotomy a 0 with lt | rfl | gt
  · obtain ⟨a, rfl⟩ : ∃ b, -b = a := ⟨-a, a.neg_neg⟩
    simp at lt
    simp [Rat.inv_neg, inv_intCast_num_of_pos lt, Int.sign_eq_one_iff_pos.mpr lt]
  · simp
  · simp [inv_intCast_num_of_pos gt, Int.sign_eq_one_iff_pos.mpr gt]

Numerator of Inverse of Integer Cast to Rationals Equals Sign of Integer

Informal description

For any integer $a$, the numerator of the inverse of the rational number obtained by casting $a$ to $\mathbb{Q}$ is equal to the sign of $a$, i.e., $\text{num}\left(\frac{1}{a}\right) = \text{sign}(a)$.

Rat.inv_natCast_num theorem

(a : ℕ) : (a : ℚ)⁻¹.num = Int.sign a

Full source

@[simp]
theorem inv_natCast_num (a : ℕ) : (a : ℚ)⁻¹.num = Int.sign a :=
  inv_intCast_num a

Numerator of Inverse of Natural Number Cast to Rationals Equals Sign of Number

Informal description

For any natural number $a$, the numerator of the inverse of the rational number obtained by casting $a$ to $\mathbb{Q}$ is equal to the sign of $a$, i.e., $\text{num}\left(\frac{1}{a}\right) = \text{sign}(a)$.

Rat.inv_ofNat_num theorem

(a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ℚ)⁻¹.num = 1

Full source

@[simp]
theorem inv_ofNat_num (a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ℚ)⁻¹.num = 1 :=
  inv_natCast_num_of_pos (Nat.pos_of_neZero a)

Numerator of Inverse of Natural Number $\geq 2$ Cast to Rationals is One

Informal description

For any natural number $a \geq 2$, the numerator of the inverse of the rational number obtained by casting $a$ to $\mathbb{Q}$ is equal to $1$, i.e., $\text{num}\left(\frac{1}{a}\right) = 1$.

Rat.inv_intCast_den theorem

(a : ℤ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a.natAbs

Full source

@[simp]
theorem inv_intCast_den (a : ℤ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a.natAbs := by
  rw [← Int.ofNat_inj]
  rcases lt_trichotomy a 0 with lt | rfl | gt
  · obtain ⟨a, rfl⟩ : ∃ b, -b = a := ⟨-a, a.neg_neg⟩
    simp at lt
    rw [if_neg (by omega)]
    simp only [Int.cast_neg, Rat.inv_neg, neg_den, inv_intCast_den_of_pos lt, Int.natAbs_neg]
    exact Int.eq_natAbs_of_nonneg (by omega)
  · simp
  · rw [if_neg (by omega)]
    simp only [inv_intCast_den_of_pos gt]
    exact Int.eq_natAbs_of_nonneg (by omega)

Denominator of Inverse of Integer Cast to Rationals: $\text{den}(1/a) = \begin{cases} 1 & \text{if } a = 0, \\ |a| & \text{otherwise.} \end{cases}$

Informal description

For any integer $a$, the denominator of the inverse of the rational number obtained by casting $a$ to $\mathbb{Q}$ is given by: \[ \text{den}\left(\frac{1}{a}\right) = \begin{cases} 1 & \text{if } a = 0, \\ |a| & \text{otherwise.} \end{cases} \]

Rat.inv_natCast_den theorem

(a : ℕ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a

Full source

@[simp]
theorem inv_natCast_den (a : ℕ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a := by
  simpa [-inv_intCast_den, ofInt_eq_cast] using inv_intCast_den a

Denominator of Inverse of Natural Number Cast to Rationals: $\text{den}(1/a) = \begin{cases} 1 & \text{if } a = 0, \\ a & \text{otherwise.} \end{cases}$

Informal description

For any natural number $a$, the denominator of the inverse of the rational number obtained by casting $a$ to $\mathbb{Q}$ is given by: \[ \text{den}\left(\frac{1}{a}\right) = \begin{cases} 1 & \text{if } a = 0, \\ a & \text{otherwise.} \end{cases} \]

Rat.inv_ofNat_den theorem

(a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ℚ)⁻¹.den = OfNat.ofNat a

Full source

@[simp]
theorem inv_ofNat_den (a : ℕ) [a.AtLeastTwo] :
    (ofNat(a) : ℚ)⁻¹.den = OfNat.ofNat a :=
  inv_natCast_den_of_pos (Nat.pos_of_neZero a)

Denominator of Inverse of Natural Number (≥2) Cast to Rationals Equals Original Number

Informal description

For any natural number $a \geq 2$, the denominator of the inverse of the rational number obtained by casting $a$ to $\mathbb{Q}$ is equal to $a$ itself, i.e., $\text{den}((a)^{-1}) = a$.

Rat.forall theorem

{p : ℚ → Prop} : (∀ r, p r) ↔ ∀ a b : ℤ, p (a / b)

Full source

protected theorem «forall» {p : ℚ → Prop} : (∀ r, p r) ↔ ∀ a b : ℤ, p (a / b) :=
  ⟨fun h _ _ => h _,
   fun h q => by
    have := h q.num q.den
    rwa [Int.cast_natCast, num_div_den q] at this⟩

Universal Quantification over Rationals via Integer Representation

Informal description

For any predicate $p$ on the rational numbers $\mathbb{Q}$, the universal quantification $\forall r \in \mathbb{Q}, p(r)$ holds if and only if for all integers $a$ and $b$, the predicate $p$ holds for the rational number $a / b$.

Rat.exists theorem

{p : ℚ → Prop} : (∃ r, p r) ↔ ∃ a b : ℤ, p (a / b)

Full source

protected theorem «exists» {p : ℚ → Prop} : (∃ r, p r) ↔ ∃ a b : ℤ, p (a / b) :=
  ⟨fun ⟨r, hr⟩ => ⟨r.num, r.den, by convert hr; convert num_div_den r⟩, fun ⟨_, _, h⟩ => ⟨_, h⟩⟩

Existence of Rational Numbers as Integer Fractions

Informal description

For any predicate $p$ on the rational numbers $\mathbb{Q}$, there exists a rational number $r$ satisfying $p(r)$ if and only if there exist integers $a$ and $b$ such that $p(a / b)$ holds.

Rat.pnatDen definition

(x : ℚ) : ℕ+

Full source

/-- Denominator as `ℕ+`. -/
def pnatDen (x : ℚ) : ℕ+ :=
  ⟨x.den, x.pos⟩

Denominator of a rational number as a positive natural number

Informal description

The function maps a rational number $ x $ to its denominator as a positive natural number, ensuring that the denominator is strictly positive.

Rat.coe_pnatDen theorem

(x : ℚ) : (x.pnatDen : ℕ) = x.den

Full source

@[simp]
theorem coe_pnatDen (x : ℚ) : (x.pnatDen : ℕ) = x.den :=
  rfl

Natural Number Cast of Positive Denominator Equals Denominator

Informal description

For any rational number $x$, the natural number obtained by casting its positive denominator $\mathrm{pnatDen}(x)$ is equal to its denominator $\mathrm{den}(x)$.

Rat.pnatDen_eq_iff_den_eq theorem

{x : ℚ} {n : ℕ+} : x.pnatDen = n ↔ x.den = ↑n

Full source

theorem pnatDen_eq_iff_den_eq {x : ℚ} {n : ℕ+} : x.pnatDen = n ↔ x.den = ↑n :=
  Subtype.ext_iff

Equivalence of Denominator Representations for Rational Numbers

Informal description

For a rational number $x$ and a positive natural number $n$, the denominator of $x$ as a positive natural number equals $n$ if and only if the denominator of $x$ as a natural number equals $n$.

Rat.pnatDen_one theorem

: (1 : ℚ).pnatDen = 1

Full source

@[simp]
theorem pnatDen_one : (1 : ℚ).pnatDen = 1 :=
  rfl

Denominator of One as Positive Natural Number is One

Informal description

The denominator of the rational number $1$ as a positive natural number is $1$, i.e., $\mathrm{pnatDen}(1) = 1$.

Rat.pnatDen_zero theorem

: (0 : ℚ).pnatDen = 1

Full source

@[simp]
theorem pnatDen_zero : (0 : ℚ).pnatDen = 1 :=
  rfl

Denominator of Zero as Positive Natural Number is One

Informal description

The denominator of the rational number $0$ as a positive natural number is $1$, i.e., $\mathrm{pnatDen}(0) = 1$.