Int.gcd_least_linear
theorem Int.gcd_least_linear : ∀ {a b : ℤ}, a ≠ 0 → IsLeast {n | 0 < n ∧ ∃ x y, ↑n = a * x + b * y} (a.gcd b) := by
sorry
This theorem states that for any two nonzero integers `a` and `b`, the greatest common divisor (gcd) of `a` and `b` is the smallest positive natural number that can be expressed as `a * x + b * y` for some integers `x` and `y`. In other words, the gcd of `a` and `b` is the least positive element of the set of all natural numbers `n` such that `n` can be written as a linear combination of `a` and `b` with integer coefficients.
More concisely: The greatest common divisor of two nonzero integers `a` and `b` is the unique positive integer `d` such that `d` can be expressed as a linear combination of `a` and `b` with integer coefficients.
|
Int.gcd_eq_one_of_gcd_mul_right_eq_one_right
theorem Int.gcd_eq_one_of_gcd_mul_right_eq_one_right : ∀ {a : ℤ} {m n : ℕ}, a.gcd (↑m * ↑n) = 1 → a.gcd ↑n = 1 := by
sorry
This theorem states that for any integer `a` and natural numbers `m` and `n`, if the greatest common divisor (gcd) of `a` and the product of `m` and `n` is `1`, then the gcd of `a` and `n` is also `1`. In mathematical terms, this can be written as: if $\gcd(a, mn) = 1$, then $\gcd(a, n) = 1$.
More concisely: If the greatest common divisor of integers `a` and `m`\*`n` is 1, then the greatest common divisor of `a` and `n` is also 1.
|
Int.dvd_gcd
theorem Int.dvd_gcd : ∀ {i j k : ℤ}, k ∣ i → k ∣ j → k ∣ ↑(i.gcd j)
The theorem `Int.dvd_gcd` states that for any three integers `i`, `j`, and `k`, if `k` divides `i` and `k` divides `j`, then `k` also divides the greatest common divisor (gcd) of `i` and `j`. The gcd here is calculated in a way that takes the absolute values of `i` and `j`, and is always a nonnegative integer. In other words, this theorem is showing a property of the gcd, that any common divisor of two numbers `i` and `j` is also a divisor of their gcd.
More concisely: If integers `i`, `j`, and `k` satisfy `k` | `i` and `k` | `j`, then `k` | gcd(`i`, `j`).
|
Int.gcd_eq_one_of_gcd_mul_right_eq_one_left
theorem Int.gcd_eq_one_of_gcd_mul_right_eq_one_left : ∀ {a : ℤ} {m n : ℕ}, a.gcd (↑m * ↑n) = 1 → a.gcd ↑m = 1 := by
sorry
This theorem states that for any integer `a` and natural numbers `m` and `n`, if the greatest common divisor (GCD) of `a` and the product of `m` and `n` is `1`, then the GCD of `a` and `m` is also `1`. In other words, if `a` is coprime with `m*n`, then `a` is also coprime with `m`. This is consistent with the properties of the GCD in mathematics.
More concisely: If the greatest common divisor of integers `a` and `m*n` is `1`, then the greatest common divisor of `a` and `m` is also `1`.
|
Nat.gcd_eq_gcd_ab
theorem Nat.gcd_eq_gcd_ab : ∀ (x y : ℕ), ↑(x.gcd y) = ↑x * x.gcdA y + ↑y * x.gcdB y
**Bézout's Lemma**: For any two natural numbers `x` and `y`, the greatest common divisor (gcd) of `x` and `y` can be expressed as a linear combination of `x` and `y`, such that `gcd x y = x * a + y * b`. Here `a` and `b` are the coefficients obtained from the extended Euclidean algorithm, represented by the functions `gcdA x y` and `gcdB x y` respectively.
More concisely: The greatest common divisor of natural numbers `x` and `y` can be expressed as a linear combination of `x` and `y`, i.e., `gcd x y = x * a + y * b` for some integers `a` and `b`.
|
Nat.xgcd_zero_left
theorem Nat.xgcd_zero_left : ∀ {s t : ℤ} {r' : ℕ} {s' t' : ℤ}, Nat.xgcdAux 0 s t r' s' t' = (r', s', t')
The theorem `Nat.xgcd_zero_left` states that for all integer values of `s` and `t` and for all natural number value of `r'` and integer values of `s'` and `t'`, when the `Nat.xgcdAux` function is invoked with the first natural number argument as zero (i.e., `0`), then the result is a triple consisting of `r'`, `s'`, and `t'`. Essentially, when the first input to the extended GCD algorithm helper function is zero, the function returns the input parameters of the second part.
More concisely: If `Nat.xgcdAux` is applied to natural number 0 and integers `s`, `t`, it returns a triple `(r', s', t')` where `r'` is a natural number and `s'`, `t'` are integers, such that `gcd(s,t) = s' * r'`.
|
Int.dvd_of_dvd_mul_right_of_gcd_one
theorem Int.dvd_of_dvd_mul_right_of_gcd_one : ∀ {a b c : ℤ}, a ∣ b * c → a.gcd b = 1 → a ∣ c
The theorem is a version of Euclid's lemma in the domain of integers. It states that for any three integers `a`, `b`, `c`, if `a` divides the product of `b` and `c` (`a ∣ b * c`) and the greatest common divisor of `a` and `b` is 1 (`gcd a b = 1`), then `a` must divide `c` (`a ∣ c`). This lemma is a key result in number theory and underpins the fundamental theorem of arithmetic. It is often used to prove that a number is prime or to establish the uniqueness of prime factorization.
More concisely: If an integer `a` divides the product of integers `b` and `c` and has a greatest common divisor of 1 with `b`, then `a` divides `c`.
|
Int.dvd_of_dvd_mul_left_of_gcd_one
theorem Int.dvd_of_dvd_mul_left_of_gcd_one : ∀ {a b c : ℤ}, a ∣ b * c → a.gcd c = 1 → a ∣ b
This is Euclid's Lemma, which states that for any integers `a`, `b`, and `c`, if `a` divides the product of `b` and `c` and the greatest common divisor of `a` and `c` is `1`, then `a` must also divide `b`. This theorem is fundamental in number theory and is also related to `IsCoprime.dvd_of_dvd_mul_left` and `UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors`.
More concisely: If integers `a`, `b`, and `c` satisfy `a` divides `bc` and `gcd(a, c) = 1`, then `a` divides `b`.
|
Int.gcd_eq_gcd_ab
theorem Int.gcd_eq_gcd_ab : ∀ (x y : ℤ), ↑(x.gcd y) = x * x.gcdA y + y * x.gcdB y
This is a statement of **Bézout's lemma** for integers. The theorem states that for any two integers `x` and `y`, the greatest common divisor of `x` and `y`, when converted to an integer (as indicated by `↑`), is equivalent to `x` multiplied by the "a" value in the extended GCD computation (as computed by `Int.gcdA`) plus `y` multiplied by the "b" value in the extended GCD computation (as computed by `Int.gcdB`). In mathematical terms, for any integers `x` and `y`, `gcd(x, y) = x * a + y * b`, where `a` and `b` are the coefficients returned by the extended GCD algorithm.
More concisely: The greatest common divisor of integers `x` and `y` is equal to `x * Int.gcdA x y + y * Int.gcdB x y`.
|
Int.coe_nat_gcd
theorem Int.coe_nat_gcd : ∀ (m n : ℕ), (↑m).gcd ↑n = m.gcd n
This theorem, named `Int.coe_nat_gcd`, states that for any two natural numbers `m` and `n`, the greatest common divisor (gcd) of `m` and `n` calculated in the domain of integers is the same as the gcd of `m` and `n` calculated in the domain of natural numbers. This is denoted as `Int.gcd ↑m ↑n = Nat.gcd m n`, where `↑m` and `↑n` represent the coercion of the natural numbers `m` and `n` to integers.
More concisely: The greatest common divisor of the coerced natural numbers to integers is equal to the greatest common divisor of the original natural numbers. In mathematical notation: `Int.gcd (coerce m to Int) (coerce n to Int) = Nat.gcd m n`.
|