Nat.gcd_div
theorem Nat.gcd_div : ∀ {m n k : ℕ}, k ∣ m → k ∣ n → (m / k).gcd (n / k) = m.gcd n / k
The theorem `Nat.gcd_div` states that for all natural numbers `m`, `n`, and `k`, if `k` divides `m` and `k` divides `n`, then the greatest common divisor (gcd) of `m / k` and `n / k` is equal to the gcd of `m` and `n` divided by `k`. In mathematical notation, this can be written as: for all $m$, $n$, $k$ in $\mathbb{N}$, if $k | m$ and $k | n$, then $\gcd(\frac{m}{k}, \frac{n}{k}) = \frac{\gcd(m, n)}{k}$.
More concisely: The greatest common divisor of `m/k` and `n/k` equals the gcd of `m` and `n` divided by `k`, for all natural numbers `m`, `n`, and `k` with `k` being a common divisor of `m` and `n`.
|
Nat.dvd_gcd_iff
theorem Nat.dvd_gcd_iff : ∀ {k : ℕ} {m n : ℕ}, k ∣ m.gcd n ↔ k ∣ m ∧ k ∣ n
This theorem states that for any natural numbers `m`, `n`, and `k`, `k` divides the greatest common divisor of `m` and `n` if and only if `k` divides `m` and `k` divides `n`. Here, "divides" is a relation denoted by `∣` in Lean 4. In terms of elementary number theory, this means that a natural number `k` is a divisor of the GCD of `m` and `n`, exactly when `k` is a common divisor of both `m` and `n`.
More concisely: The greatest common divisor of natural numbers `m` and `n` equals the least common multiple of their divisors `k` if and only if `k` divides both `m` and `n`. equivalently, `k` is a common divisor of `m` and `n` if and only if it divides their GCD.
|
Nat.gcd_dvd_right
theorem Nat.gcd_dvd_right : ∀ (m n : ℕ), m.gcd n ∣ n
This theorem states that for every pair of natural numbers `m` and `n`, the greatest common divisor (gcd) of `m` and `n` divides `n`. In mathematical notation, this can be written as: "For all m, n in ℕ, gcd(m, n) ∣ n". This is a fundamental property of the gcd in number theory.
More concisely: The greatest common divisor of natural numbers `m` and `n` (gcd(m, n)) is a divisor of `n` (gcd(m, n) | n).
|
Nat.gcd_dvd_left
theorem Nat.gcd_dvd_left : ∀ (m n : ℕ), m.gcd n ∣ m
The theorem `Nat.gcd_dvd_left` states that for all natural numbers `m` and `n`, the greatest common divisor (gcd) of `m` and `n` divides `m`. In other words, `m` is a multiple of the gcd of `m` and `n`. This is a fundamental property of the gcd in number theory.
More concisely: The greatest common divisor of natural numbers `m` and `n` (gcd `m` `n`) divides `m` (`gcd` `m` `n` | `m`).
|
Nat.gcd.induction
theorem Nat.gcd.induction :
∀ {P : ℕ → ℕ → Prop} (m n : ℕ), (∀ (n : ℕ), P 0 n) → (∀ (m n : ℕ), 0 < m → P (n % m) m → P m n) → P m n
This theorem is a principle of induction for the greatest common divisor (gcd) on two natural numbers, denoted as `P m n`. Given two natural numbers `m` and `n`, it states that if a property `P` holds for all natural numbers `n` when `m` is 0, and if for any `m` and `n` with `m` greater than 0, the property `P` holds for `n mod m` and `m` whenever it holds for `m` and `n`, then the property `P` holds for any `m` and `n`. This can be used to create proofs that rely on the properties of the gcd and the division operation.
More concisely: If `P` is a property that holds for all natural numbers `n` when the first number `m` is 0, and `P` holds for `n` when `m` is greater than 0 if and only if it holds for `n mod m` and `m`, then `P` holds for all natural numbers `m` and `n`.
|
Nat.gcd_zero_left
theorem Nat.gcd_zero_left : ∀ (y : ℕ), Nat.gcd 0 y = y
The theorem `Nat.gcd_zero_left` states that for any natural number `y`, the greatest common divisor of 0 and `y` is `y` itself. In other words, it formalizes the mathematical property $\gcd(0,y) = y$ for all natural numbers `y`.
More concisely: The greatest common divisor of 0 and any natural number `y` equals `y`.
|
Nat.gcd_dvd
theorem Nat.gcd_dvd : ∀ (m n : ℕ), m.gcd n ∣ m ∧ m.gcd n ∣ n
The theorem `Nat.gcd_dvd` states that for all natural numbers `m` and `n`, the greatest common divisor (GCD) of `m` and `n` is a divisor of both `m` and `n`. In other words, the GCD of two numbers divides each of the two numbers. This is a fundamental property of the GCD, typically denoted mathematically as $\text{gcd}(m, n) | m$ and $\text{gcd}(m, n) | n$.
More concisely: The greatest common divisor of natural numbers m and n (denoted as gcd(m, n)) is a divisor of both m and n. In Lean notation: ∀ (m n : ℕ), gcd m n ∣ m ∧ gcd m n ∣ n.
|
Nat.gcd_one_left
theorem Nat.gcd_one_left : ∀ (n : ℕ), Nat.gcd 1 n = 1
This theorem states that for any natural number `n`, the greatest common divisor of 1 and `n` is 1. This result aligns with the mathematical principle that the greatest common divisor of any number and 1 is always 1.
More concisely: The greatest common divisor of 1 and any natural number `n` equals 1.
|
Nat.gcd_eq_left
theorem Nat.gcd_eq_left : ∀ {m n : ℕ}, m ∣ n → m.gcd n = m
This theorem states that for all natural numbers `m` and `n`, if `m` divides `n` (denoted as `m ∣ n`), then the greatest common divisor (gcd) of `m` and `n` is `m` itself. In other words, if a number `m` is a divisor of another number `n`, then `m` is the largest number that can divide both `m` and `n` without leaving a remainder.
More concisely: If `m` divides `n`, then `gcd m n = m`.
|
Nat.gcd_pos_of_pos_left
theorem Nat.gcd_pos_of_pos_left : ∀ {m : ℕ} (n : ℕ), 0 < m → 0 < m.gcd n
The theorem `Nat.gcd_pos_of_pos_left` states that for all natural numbers `m` and `n`, if `m` is greater than 0, then the greatest common divisor (gcd) of `m` and `n` is also greater than 0. In other words, if a natural number `m` is positive, its gcd with any other natural number `n` is also positive.
More concisely: For all natural numbers m and n, if m > 0 then gcd(m, n) > 0.
|
Nat.eq_zero_of_gcd_eq_zero_left
theorem Nat.eq_zero_of_gcd_eq_zero_left : ∀ {m n : ℕ}, m.gcd n = 0 → m = 0
The theorem `Nat.eq_zero_of_gcd_eq_zero_left` states that for any two natural numbers `m` and `n`, if the greatest common divisor (gcd) of `m` and `n` is zero, then `m` must be zero. In mathematical terms, this can be expressed as: for all natural numbers `m` and `n`, if `gcd(m, n) = 0`, then `m = 0`.
More concisely: If the greatest common divisor of natural numbers `m` and `n` is zero, then `m` equals zero.
|
Nat.gcd_one_right
theorem Nat.gcd_one_right : ∀ (n : ℕ), n.gcd 1 = 1
This theorem, `Nat.gcd_one_right`, states that for any natural number `n`, the greatest common divisor (GCD) of `n` and `1` is `1`. In other words, the greatest common divisor of any natural number and `1` is always `1` itself. This aligns with the general mathematical understanding that `1` is a divisor of every natural number.
More concisely: The greatest common divisor of any natural number and 1 is 1.
|
Nat.gcd_eq_right
theorem Nat.gcd_eq_right : ∀ {m n : ℕ}, n ∣ m → m.gcd n = n
This theorem states that for any two natural numbers `m` and `n`, if `n` divides `m` then the greatest common divisor (gcd) of `m` and `n` is `n`. In other words, if `n` is a divisor of `m`, it's the largest possible common divisor of both `m` and `n`.
More concisely: If `n` divides `m`, then the greatest common divisor of `m` and `n` equals `n`.
|
Nat.dvd_gcd
theorem Nat.dvd_gcd : ∀ {k m n : ℕ}, k ∣ m → k ∣ n → k ∣ m.gcd n
This theorem states that for all natural numbers `k`, `m`, and `n`, if `k` divides `m` and `k` divides `n`, then `k` also divides the greatest common divisor of `m` and `n`. In mathematical terms, we can express it as follows: for all $k, m, n \in \mathbb{N}$, if $k | m$ and $k | n$, then $k | \gcd(m, n)$.
More concisely: If `k` divides `m` and `k` divides `n`, then `k` divides their greatest common divisor `gcd(m, n)`.
|
Nat.gcd_zero_right
theorem Nat.gcd_zero_right : ∀ (n : ℕ), n.gcd 0 = n
This theorem, `Nat.gcd_zero_right`, states that for any natural number `n`, the greatest common divisor (gcd) of `n` and `0` is `n` itself. In other words, if you compute the gcd between any natural number and zero, you will always get the original natural number. This is a standard result in number theory and is represented mathematically as $\text{gcd}(n, 0) = n$ for any natural number $n$.
More concisely: The greatest common divisor of a natural number `n` and zero is equal to `n`. In Lean, this is expressed as `Nat.gcd_zero_right n`.
|
Nat.gcd_rec
theorem Nat.gcd_rec : ∀ (m n : ℕ), m.gcd n = (n % m).gcd m
This theorem, `Nat.gcd_rec`, asserts that for all natural numbers `m` and `n`, the greatest common divisor (gcd) of `m` and `n` is equal to the gcd of the remainder of `n` divided by `m` (`n % m`) and `m`. This theorem is a key part of Euclid's algorithm for finding the greatest common divisor of two numbers. In mathematical terms, it states that for all $m, n \in \mathbb{N}$, $\gcd(m, n) = \gcd(n \mod m, m)$.
More concisely: The greatest common divisor of two natural numbers is equal to the greatest common divisor of their remainder when one is divided by the other, and the dividing number.
|
Nat.gcd_eq_left_iff_dvd
theorem Nat.gcd_eq_left_iff_dvd : ∀ {m n : ℕ}, m ∣ n ↔ m.gcd n = m
This theorem states that for any two natural numbers `m` and `n`, `m` divides `n` if and only if the greatest common divisor (gcd) of `m` and `n` is `m` itself. In other words, if `m` is a divisor of `n`, then `m` must be the greatest common divisor of `m` and `n`; conversely, if the gcd of `m` and `n` is `m`, then `m` is a divisor of `n`.
More concisely: The natural numbers `m` and `n` are equivalent, up to ordering, to `m` being a divisor of `n` if and only if the greatest common divisor of `m` and `n` equals `m`.
|
Nat.gcd_ne_zero_right
theorem Nat.gcd_ne_zero_right : ∀ {n m : ℕ}, n ≠ 0 → m.gcd n ≠ 0
The theorem `Nat.gcd_ne_zero_right` states that for all natural numbers `n` and `m`, if `n` is not equal to zero, then the greatest common divisor (gcd) of `m` and `n` is also not equal to zero. In mathematical terms, this translates to "For all natural numbers m and n, if n ≠ 0, then gcd(m, n) ≠ 0.".
More concisely: If a natural number `n` is non-zero, then the greatest common divisor of `n` and another natural number `m` is also non-zero.
|
Nat.gcd_dvd_gcd_of_dvd_left
theorem Nat.gcd_dvd_gcd_of_dvd_left : ∀ {m k : ℕ} (n : ℕ), m ∣ k → m.gcd n ∣ k.gcd n
The theorem `Nat.gcd_dvd_gcd_of_dvd_left` states that for all natural numbers `m`, `k`, and `n`, if `m` divides `k`, then the greatest common divisor (gcd) of `m` and `n` divides the gcd of `k` and `n`. In mathematical notation, this is saying that for all m, k, n ∈ ℕ, if m | k, then gcd(m, n) | gcd(k, n).
More concisely: If `m` divides `k`, then the greatest common divisor of `m` and `n` (gcd(m, n)) is a divisor of the greatest common divisor of `k` and `n` (gcd(k, n)).
|
Nat.gcd_comm
theorem Nat.gcd_comm : ∀ (m n : ℕ), m.gcd n = n.gcd m
This theorem, `Nat.gcd_comm`, states that for all natural numbers `m` and `n`, the greatest common divisor (gcd) of `m` and `n` is the same as the gcd of `n` and `m`. In other words, the order in which the numbers are passed to the gcd function does not matter, making the gcd function commutative. This mirrors the mathematical property that $\gcd(m, n) = \gcd(n, m)$ for any natural numbers $m$ and $n$.
More concisely: The greatest common divisor of natural numbers `m` and `n` is commutative, i.e., `gcd m n = gcd n m`.
|
Nat.gcd_pos_of_pos_right
theorem Nat.gcd_pos_of_pos_right : ∀ (m : ℕ) {n : ℕ}, 0 < n → 0 < m.gcd n
This theorem states that for any two natural numbers `m` and `n`, if `n` is positive (greater than 0), then the greatest common divisor (gcd) of `m` and `n` is also positive. In mathematical terms, it asserts that for all natural numbers `m` and `n`, where `n > 0`, the greatest common divisor `gcd(m, n) > 0`.
More concisely: For all natural numbers `m` and `n` with `n > 0`, the greatest common divisor `gcd(m, n)` is a positive number.
|
Nat.gcd_self
theorem Nat.gcd_self : ∀ (n : ℕ), n.gcd n = n
This theorem states that for every natural number `n`, the greatest common divisor (gcd) of `n` and `n` is `n` itself. In other words, the gcd of a number with itself is always the number itself. This is a property of the gcd function in the natural numbers domain.
More concisely: The greatest common divisor of a natural number with itself is the number itself. (gcd (n : ℕ) (n : ℕ)) = n for all natural numbers n.
|
Nat.gcd_mul_left
theorem Nat.gcd_mul_left : ∀ (m n k : ℕ), (m * n).gcd (m * k) = m * n.gcd k
This theorem states that for any three natural numbers `m`, `n`, and `k`, the greatest common divisor of `m * n` and `m * k` is equal to `m` times the greatest common divisor of `n` and `k`. This is a property of the gcd operation that shows how it interacts with multiplication, highlighting its distributive nature.
More concisely: The greatest common divisor of `m * n` and `m * k` is equal to `m` times the greatest common divisor of `n` and `k`.
|
Nat.eq_zero_of_gcd_eq_zero_right
theorem Nat.eq_zero_of_gcd_eq_zero_right : ∀ {m n : ℕ}, m.gcd n = 0 → n = 0
The theorem `Nat.eq_zero_of_gcd_eq_zero_right` states that for all natural numbers `m` and `n`, if the greatest common divisor (gcd) of `m` and `n` is zero, then `n` must be zero. This theorem is stating a property of the gcd function on natural numbers in the context of number theory.
More concisely: If the greatest common divisor of natural numbers `m` and `n` is zero, then `n` is equal to zero.
|
Nat.gcd_mul_right
theorem Nat.gcd_mul_right : ∀ (m n k : ℕ), (m * n).gcd (k * n) = m.gcd k * n
This theorem states that for any three natural numbers `m`, `n`, and `k`, the greatest common divisor (gcd) of the product of `m` and `n`, and the product of `k` and `n`, is equal to the product of the gcd of `m` and `k`, and `n`. That means, in mathematical terms, we have $\gcd(mn, kn) = \gcd(m, k) \cdot n$ for all natural numbers `m`, `n`, `k`.
More concisely: The theorem asserts that the greatest common divisor of the products of two natural numbers with a common factor is equal to the product of their greatest common divisor and the common factor. In other words, $\gcd(mn, kn) = \gcd(m, k) \cdot n$.
|
Nat.gcd_eq_iff
theorem Nat.gcd_eq_iff : ∀ {g : ℕ} (a b : ℕ), a.gcd b = g ↔ g ∣ a ∧ g ∣ b ∧ ∀ (c : ℕ), c ∣ a → c ∣ b → c ∣ g
This theorem provides a characterization of the greatest common divisor (gcd) of two natural numbers `a` and `b`. Specifically, it states that for any natural number `g`, `g` equals the gcd of `a` and `b` if and only if three conditions are met: `g` divides both `a` and `b`, and any natural number `c` that divides both `a` and `b` must also divide `g`. This result encapsulates both the divisibility properties and the maximality condition that define the greatest common divisor in number theory.
More concisely: The greatest common divisor of natural numbers `a` and `b` is the unique natural number `g` that divides both `a` and `b`, and any number that divides both `a` and `b` also divides `g`.
|