Rat.reduced
theorem Rat.reduced : ∀ (self : ℚ), self.num.natAbs.Coprime self.den
This theorem states that for any rational number, the absolute value of its numerator and its denominator are coprime. In other words, the greatest common divisor of the numerator and the denominator of any rational number is 1. This is a form of simplifying rational numbers where the numerator and the denominator have no common factors other than 1, also known as "reduced form".
More concisely: The greatest common divisor of any rational number's numerator and denominator equals 1.
|
Rat.add.aux
theorem Rat.add.aux :
∀ (a b : ℚ) {g ad bd : ℕ},
g = a.den.gcd b.den →
ad = a.den / g →
bd = b.den / g →
let den := ad * b.den;
let num := a.num * ↑bd + b.num * ↑ad;
num.natAbs.gcd g = num.natAbs.gcd den
This theorem, `Rat.add.aux`, is about the addition of rational numbers. For any two rational numbers `a` and `b`, and given natural numbers `g`, `ad`, `bd` such that `g` is the greatest common divisor (gcd) of the denominators of `a` and `b`, `ad` is the denominator of `a` divided by `g`, and `bd` is the denominator of `b` divided by `g`, the theorem states that the gcd of the absolute value of the sum of the numerators of `a` and `b` (each multiplied by `bd` and `ad` respectively) and `g` is equal to the gcd of the same sum and the product of `ad` and the denominator of `b`. This result plays an essential role in the arithmetic of rational numbers.
More concisely: Given rational numbers `a` and `b` with gcd(denominator(`a`), denominator(`b`)) = `g`, the gcd of (numerator(`a`) * denominator(`b`) / `g` + numerator(`b`) * denominator(`a`) / `g`) and `g` is equal to gcd((numerator(`a`) / `ad` + numerator(`b`) / `bd`), `g`), where `ad` = denominator(`a`) / `g` and `bd` = denominator(`b`) / `g`.
|
Rat.den_nz
theorem Rat.den_nz : ∀ (self : ℚ), self.den ≠ 0
The theorem `Rat.den_nz` asserts that for any rational number, its denominator is not zero. In other words, when we represent a rational number in the form of a fraction, the denominator of that fraction can never be zero.
More concisely: The theorem `Rat.den_nz` asserts that the denominator of a rational number is never equal to zero.
|
Rat.den_pos
theorem Rat.den_pos : ∀ (self : ℚ), 0 < self.den
This theorem, `Rat.den_pos`, states that for any rational number, its denominator is always greater than zero. In other words, no matter what rational number you have, its denominator will never be zero or negative.
More concisely: The denominator of every rational number is positive.
|