Nat.gcd_add_mul_left_right
theorem Nat.gcd_add_mul_left_right : ∀ (m n k : ℕ), m.gcd (n + m * k) = m.gcd n
This theorem states that for all natural numbers `m`, `n`, and `k`, the greatest common divisor (GCD) of `m` and `n` added to `m` times `k` (`n + m * k`) is equal to the GCD of `m` and `n`. In mathematical notation, it states that $\gcd(m, n+mk) = \gcd(m, n)$ for all natural numbers $m, n, k$. This property reflects the distributive nature of the GCD operation over addition and multiplication.
More concisely: The greatest common divisor of two numbers is unchanged when one number is replaced with another number that is the first number multiplied by a third number and added to the second number. In mathematical notation, $\gcd(m, n) = \gcd(m, n + mk)$ for all natural numbers $m, n, k$.
|
Nat.gcd_add_self_right
theorem Nat.gcd_add_self_right : ∀ (m n : ℕ), m.gcd (n + m) = m.gcd n
The theorem `Nat.gcd_add_self_right` states that for all natural numbers `m` and `n`, the greatest common divisor (gcd) of `m` and `n + m` is the same as the gcd of `m` and `n`. In mathematical terms, it says that for any two natural numbers $m$ and $n$, we have $\gcd(m, n + m) = \gcd(m, n)$.
More concisely: The greatest common divisor of a natural number with another number is unchanged when the second number is replaced by their sum with the first number. In mathematical notation, this is expressed as $\gcd(m, n) = \gcd(m, n+m)$.
|
Nat.eq_one_of_dvd_coprimes
theorem Nat.eq_one_of_dvd_coprimes : ∀ {a b k : ℕ}, a.Coprime b → k ∣ a → k ∣ b → k = 1
This theorem states that for any three natural numbers `a`, `b`, and `k`, if `a` and `b` are coprime (i.e., their greatest common divisor is 1) and `k` divides both `a` and `b`, then `k` must be equal to 1.
More concisely: If natural numbers `a`, `b`, and `k` satisfy `gcd(a, b) = 1` and `k` | `a` and `k` | `b`, then `k = 1`.
|
Nat.gcd_add_self_left
theorem Nat.gcd_add_self_left : ∀ (m n : ℕ), (m + n).gcd n = m.gcd n
The theorem `Nat.gcd_add_self_left` states that for any two natural numbers `m` and `n`, the greatest common divisor (GCD) of `m + n` and `n` is equal to the GCD of `m` and `n`. In other words, adding `n` to `m` does not change the greatest common divisor of `m` and `n`. This is a property of the greatest common divisor in number theory.
More concisely: The theorem asserts that for all natural numbers m and n, the greatest common divisor of m + n and n is equal to the greatest common divisor of m and n. In Lean notation: `(∀ m n : ℕ, gcd m (m + n) = gcd m n)`.
|
Nat.lcm_dvd_mul
theorem Nat.lcm_dvd_mul : ∀ (m n : ℕ), m.lcm n ∣ m * n
This theorem states that for any two natural numbers `m` and `n`, the least common multiple of `m` and `n` divides the product of `m` and `n`. In mathematical terms, if `lcm(m, n)` denotes the least common multiple of `m` and `n`, then there exists a natural number `k`, such that `m * n = k * lcm(m, n)`.
More concisely: The least common multiple of natural numbers `m` and `n` divides their product. In other words, `lcm(m, n) | (m * n)`.
|
Nat.lcm_dvd_iff
theorem Nat.lcm_dvd_iff : ∀ {m n k : ℕ}, m.lcm n ∣ k ↔ m ∣ k ∧ n ∣ k
The theorem `Nat.lcm_dvd_iff` states that for any three natural numbers `m`, `n`, and `k`, the least common multiple of `m` and `n` divides `k` if and only if both `m` and `n` divide `k`. Here, the least common multiple of `m` and `n` is defined as the product of `m` and `n`, divided by their greatest common divisor.
More concisely: The least common multiple of natural numbers m and n divides k if and only if both m and n divide k. (Equivalently, m and n have product d such that k is divisible by d if and only if m and n are divisors of k.)
|
Nat.gcd_add_mul_right_right
theorem Nat.gcd_add_mul_right_right : ∀ (m n k : ℕ), m.gcd (n + k * m) = m.gcd n
The theorem `Nat.gcd_add_mul_right_right` states that for all natural numbers `m`, `n`, and `k`, the greatest common divisor (gcd) of `m` and `n + k * m` is the same as the gcd of `m` and `n`. In other words, multiplying `m` by `k` and adding the result to `n` does not change the gcd of `m` and `n`. This property is crucial in many number theoretic algorithms and proofs involving greatest common divisors.
More concisely: The theorem `Nat.gcd_add_mul_right_right` asserts that adding the product of a natural number `k` with another natural number `m` to another natural number `n` does not alter the greatest common divisor of `m` and `n`. In other words, gcd(`m`, `n`) = gcd(`m`, `n` + `k` * `m`).
|