Rat.zero_mkRat
theorem Rat.zero_mkRat : ∀ (n : ℕ), mkRat 0 n = 0
This theorem, `Rat.zero_mkRat`, states that for any natural number `n`, creating a rational number using `mkRat` with 0 as the numerator and `n` as the denominator yields the rational number 0. It underscores the standard mathematical principle that any fraction with a zero numerator is equal to zero, regardless of the denominator (assuming it's not zero, as the domain here is natural numbers, excluding 0).
More concisely: For any natural number `n`, the rational number `mkRat 0 n` equals the rational number 0.
|
Rat.zero_divInt
theorem Rat.zero_divInt : ∀ (n : ℤ), Rat.divInt 0 n = 0
The theorem `Rat.zero_divInt` states that for any integer `n`, the result of the function `Rat.divInt` with the first argument as 0 and the second argument as `n` is always 0. In mathematical terms, it is equivalent to saying that $\frac{0}{n} = 0$ for any integer `n`.
More concisely: The theorem asserts that for all integers `n`, the quotient of 0 by `n` is equal to 0 in the `Rat` type of Lean. In mathematical notation, $\text{Rat}(0/n) = 0$.
|
Rat.divInt_neg'
theorem Rat.divInt_neg' : ∀ (num den : ℤ), Rat.divInt num (-den) = Rat.divInt (-num) den
This theorem, `Rat.divInt_neg'`, states that for any two integers `num` and `den`, the quotient of `num` divided by the negative of `den` is equal to the quotient of the negative of `num` divided by `den`. In other words, it confirms the mathematical rule that the division of a number by a negative number is the same as dividing the negative of that number by the positive counterpart. This is typically expressed in mathematical notation as $\frac{num}{-den} = \frac{-num}{den}$.
More concisely: The theorem `Rat.divInt_neg'` asserts that for all integers `num` and `den`, `num / (-den) = -(num / den)`.
|
Rat.divInt_ofNat
theorem Rat.divInt_ofNat : ∀ (num : ℤ) (den : ℕ), Rat.divInt num ↑den = mkRat num den
The theorem `Rat.divInt_ofNat` states that for every pair of integers `num` and natural number `den`, the result of dividing `num` by the integer representation of `den` using the `Rat.divInt` function is equal to the result of constructing a rational number with `num` as the numerator and `den` as the denominator using the `mkRat` function. Essentially, this theorem asserts the consistency between integer division and the construction of a rational number in the Lean 4 mathematical library.
More concisely: For every integer `num` and natural number `den`, `Rat.divInt num den` equals `Rat.mkRat num den`.
|
Rat.normalize_eq_mkRat
theorem Rat.normalize_eq_mkRat :
∀ {num : ℤ} {den : ℕ} (den_nz : den ≠ 0), Rat.normalize num den den_nz = mkRat num den
This theorem states that for any integer `num` and natural number `den` where `den` is not equal to zero, the rational number obtained by normalizing `num` and `den` using `Rat.normalize` is equivalent to the rational number obtained by constructing it using `mkRat`. Essentially, it shows that the smart constructors `Rat.normalize` and `mkRat` yield the same result when the denominator is not zero.
More concisely: For any integer `num` and natural number `den`, the rational numbers `Rat.normalize num den` and `mkRat num den` are equal when `den` is non-zero.
|
Rat.mk_eq_normalize
theorem Rat.mk_eq_normalize :
∀ (num : ℤ) (den : ℕ) (nz : den ≠ 0) (c : num.natAbs.Coprime den),
{ num := num, den := den, den_nz := nz, reduced := c } = Rat.normalize num den nz
This theorem states that for any integer `num` and any natural number `den` that is not zero, if `num` and `den` are coprime (their greatest common divisor is 1), then creating a rational number with `num` as the numerator and `den` as the denominator is equivalent to normalizing the rational number with the same numerator and denominator. In other words, if the absolute value of the numerator and the denominator are coprime, then the rational number is already in its simplest or reduced form, and normalization does not change it.
More concisely: If `num` and `den` are coprime integers, then the rational number `num / den` is equal to the rational number obtained by normalizing `num` and `den`.
|
Rat.add_def
theorem Rat.add_def : ∀ (a b : ℚ), a + b = Rat.normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯
This theorem states that for any two rational numbers `a` and `b`, the sum of `a` and `b` is equal to the rational number constructed by normalizing the sum of the product of the numerator of `a` and the denominator of `b` and the product of the numerator of `b` and the denominator of `a`, where the denominator of the resulting rational number is the product of the denominators of `a` and `b`. In mathematical terms, if $a = \frac{a_{num}}{a_{den}}$ and $b = \frac{b_{num}}{b_{den}}$, then $a + b = \frac{a_{num} \cdot b_{den} + b_{num} \cdot a_{den}}{a_{den} \cdot b_{den}}$, where the numerator and denominator of the resulting fraction are divided by their greatest common divisor to ensure the fraction is in its simplest form.
More concisely: For any rational numbers `a = a_num/a_den` and `b = b_num/b_den`, the sum `a + b` equals the rational number `(a_num * b_den + b_num * a_den) / (a_den * b_den)` in its simplest form.
|
Rat.normalize_zero
theorem Rat.normalize_zero : ∀ {d : ℕ} (nz : d ≠ 0), Rat.normalize 0 d nz = 0
The theorem `Rat.normalize_zero` states that for any natural number `d` that is not zero, if we use the `Rat.normalize` function to normalize zero and `d`, the result will be zero. In other words, the normalized form of the rational number formed by the integer 0 and any non-zero natural number `d` is always 0.
More concisely: For any non-zero natural number `d`, `Rat.normalize 0 d` equals zero.
|
Rat.mk_eq_divInt
theorem Rat.mk_eq_divInt :
∀ (num : ℤ) (den : ℕ) (nz : den ≠ 0) (c : num.natAbs.Coprime den),
{ num := num, den := den, den_nz := nz, reduced := c } = Rat.divInt num ↑den
This theorem states that for every integer `num` and natural number `den` where `den` is not equal to zero, as well as when `num` and `den` are coprime (i.e., their greatest common divisor is 1), the rational number `{ num := num, den := den, den_nz := nz, reduced := c }` is equal to the result of the division `num / den` in the rational numbers. The coprimeness is calculated with respect to the absolute value of `num`.
More concisely: For integers `num` and `den` with `den ≠ 0` and `gcd(|num|, |den|) = 1`, the rational number `{num := num, den := den, den_nz := nz, reduced := c}` equals `num / den` in the rational numbers.
|
Rat.mul_def
theorem Rat.mul_def : ∀ (a b : ℚ), a * b = Rat.normalize (a.num * b.num) (a.den * b.den) ⋯
This theorem states that for any two rational numbers `a` and `b`, the product `a * b` is equal to the result of normalizing the rational number formed by multiplying the numerators of `a` and `b` as the new numerator and the denominators of `a` and `b` as the new denominator. The normalization process involves dividing the numerator and the denominator by their greatest common divisor (gcd) to ensure the resulting rational number is in its simplest form.
More concisely: For any rational numbers `a` and `b`, `a * b` is equivalent to the rational number obtained by multiplying the numerators of `a` and `b` and then normalizing the result by dividing numerator and denominator by their greatest common divisor.
|
Rat.divInt_zero
theorem Rat.divInt_zero : ∀ (n : ℤ), Rat.divInt n 0 = 0
The theorem `Rat.divInt_zero` states that for any integer `n`, the function `Rat.divInt` returns zero when the second argument is zero. In other words, when dividing any integer by zero, the result is always zero. This is mathematically represented as ∀ n ∈ ℤ, n / 0 = 0.
More concisely: For all integers n, the quotient of n and 0 is equal to zero.
|
Rat.divInt_mul_right
theorem Rat.divInt_mul_right : ∀ {n d a : ℤ}, a ≠ 0 → Rat.divInt (n * a) (d * a) = Rat.divInt n d
This theorem, `Rat.divInt_mul_right`, states that for all integer values `n`, `d`, and `a`, if `a` is not equal to zero, then the result of dividing the product of `n` and `a` by the product of `d` and `a` (using the `Rat.divInt` function) is the same as the result of dividing `n` by `d` (also using the `Rat.divInt` function). Essentially, it depicts a property of division in the rational numbers: the multiplication of both the numerator and the denominator by a non-zero integer does not affect the value of the fraction. This is equivalent to the mathematical statement: ∀n, d, a ∈ ℤ, a ≠ 0 → n/d = (n*a)/(d*a).
More concisely: For all integers n, d, and a not equal to zero, (n * a) / (d * a) equals n / d.
|
Rat.normalize_eq
theorem Rat.normalize_eq :
∀ {num : ℤ} {den : ℕ} (den_nz : den ≠ 0),
Rat.normalize num den den_nz =
{ num := num / ↑(num.natAbs.gcd den), den := den / num.natAbs.gcd den, den_nz := ⋯, reduced := ⋯ }
This theorem states that, for any integer `num` and any non-zero natural number `den`, the rational number obtained by normalizing `num` over `den` is equal to the rational number whose numerator is `num` divided by the greatest common divisor (gcd) of the absolute value of `num` and `den`, and whose denominator is `den` divided by the same gcd. Here, the normalization process involves dividing both the numerator and the denominator by their gcd to ensure that the resulting rational number is in its simplest or reduced form.
More concisely: For any integer `num` and non-zero natural number `den`, the rational number `num / gcd(abs(num), den)` is equal to the rational number `(num / abs(num)) / (den / gcd(abs(num), den))`, where `gcd` denotes the greatest common divisor.
|
Rat.divInt_eq_iff
theorem Rat.divInt_eq_iff :
∀ {d₁ d₂ n₁ n₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → (Rat.divInt n₁ d₁ = Rat.divInt n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁)
This theorem states that for any four integers `d₁`, `d₂`, `n₁`, and `n₂`, where `d₁` and `d₂` are not zero, the rational number formed by dividing `n₁` by `d₁` is equal to the rational number formed by dividing `n₂` by `d₂` if and only if the cross product of `n₁` and `d₂` is equal to the cross product of `n₂` and `d₁`. In other words, $\frac{n_1}{d_1} = \frac{n_2}{d_2}$ if and only if $n_1 \cdot d_2 = n_2 \cdot d_1$.
More concisely: Two rational numbers $\frac{n\_1}{d\_1}$ and $\frac{n\_2}{d\_2}$ are equal if and only if their numerators have the same cross product with the denominators: $n\_1 \cdot d\_2 = n\_2 \cdot d\_1$.
|
Rat.normalize_self
theorem Rat.normalize_self : ∀ (r : ℚ), Rat.normalize r.num r.den ⋯ = r
The theorem `Rat.normalize_self` states that for any rational number `r`, if we normalize `r` by taking its numerator and denominator and use them as arguments for the `Rat.normalize` function, the output is equal to the original rational number `r` itself. In other words, normalizing a rational number using its own numerator and denominator results in the same rational number.
More concisely: For any rational number r, normalizing r using its numerator and denominator yields the same rational number (i.e., Rat.normalize (numerator r) (denominator r) = r).
|
Rat.normalize_mul_left
theorem Rat.normalize_mul_left :
∀ {d : ℕ} {n : ℤ} {a : ℕ} (d0 : d ≠ 0) (a0 : a ≠ 0), Rat.normalize (↑a * n) (a * d) ⋯ = Rat.normalize n d d0 := by
sorry
The theorem `Rat.normalize_mul_left`, states that for every integer `n`, and non-zero natural numbers `d` and `a`, the result of normalizing the rational number whose numerator is `a * n` and denominator is `a * d` is the same as the result of normalizing the rational number whose numerator is `n` and denominator is `d`. In other words, multiplication of the numerator and denominator of a rational number by a non-zero natural number `a` does not change the normalized value of the rational number. Here, normalization refers to the process of dividing the numerator and denominator by their greatest common divisor to ensure the resulting rational number is in its simplest form.
More concisely: For any integer `n`, non-zero natural number `d`, and rational number `a/b`, normalizing the rational number `a * (n/d)` equals normalizing `(a/b) * n/d`.
|
Rat.mkRat_zero
theorem Rat.mkRat_zero : ∀ (n : ℤ), mkRat n 0 = 0
This theorem states that for every integer `n`, when we create a rational number with `n` as the numerator and `0` as the denominator using the `mkRat` function, we will always get `0`. This is consistent with the definition of `mkRat`, which ensures that when the denominator is zero, the function returns zero, regardless of the value of the numerator.
More concisely: For every integer `n`, the rational number `mkRat n 0` equals `0`.
|
Rat.mul_comm
theorem Rat.mul_comm : ∀ (a b : ℚ), a * b = b * a
This theorem states that multiplication of rational numbers is commutative. In other words, for any two rational numbers 'a' and 'b', the result of 'a' multiplied by 'b' is the same as 'b' multiplied by 'a'.
More concisely: For all rational numbers a and b, a * b = b * a.
|