Nat.dvd_mul_left
theorem Nat.dvd_mul_left : ∀ (a b : ℕ), a ∣ b * a
This theorem states that for any two natural numbers `a` and `b`, `a` is a divisor of the product of `b` and `a`. In the context of number theory, if we multiply `a` with any natural number `b`, `a` will always divide the resulting product.
More concisely: For all natural numbers a and b, a divides the product b * a.
|
Nat.pos_of_dvd_of_pos
theorem Nat.pos_of_dvd_of_pos : ∀ {m n : ℕ}, m ∣ n → 0 < n → 0 < m
This theorem, `Nat.pos_of_dvd_of_pos`, states that for any two natural numbers `m` and `n`, if `m` divides `n` and `n` is greater than 0, then `m` is also greater than 0. In terms of number theory, it asserts that a non-zero number cannot be divided by zero, since division by zero is undefined.
More concisely: If `m` divides `n` and `n` is positive, then `m` is also positive.
|
Nat.dvd_of_mod_eq_zero
theorem Nat.dvd_of_mod_eq_zero : ∀ {m n : ℕ}, n % m = 0 → m ∣ n
This theorem, `Nat.dvd_of_mod_eq_zero`, states that for all natural numbers `m` and `n`, if the remainder of `n` divided by `m` (`n % m`) is zero, then `m` divides `n` (`m ∣ n`). In other words, if `n` is divisible by `m` without leaving a remainder, then `m` is a divisor of `n`. This is a basic property of divisibility in the domain of natural numbers.
More concisely: If `n` is congruent to 0 modulo `m`, then `m` divides `n`. (In mathematical notation: `m ∣ n <-> n % m = 0`)
|
Nat.eq_one_of_dvd_one
theorem Nat.eq_one_of_dvd_one : ∀ {n : ℕ}, n ∣ 1 → n = 1
This theorem states that for any natural number `n`, if `n` divides 1, then `n` must be equal to 1. In mathematical terms, it asserts that if `n` is a divisor of 1 in the set of natural numbers, its value has to be 1. This is because 1 is the only natural number that can divide 1 to yield another natural number.
More concisely: If a natural number `n` divides 1, then `n` equals 1.
|
Nat.mod_mod_of_dvd
theorem Nat.mod_mod_of_dvd : ∀ {c b : ℕ} (a : ℕ), c ∣ b → a % b % c = a % c
This theorem, `Nat.mod_mod_of_dvd`, states that for any natural numbers 'a', 'b', and 'c', if 'c' divides 'b', then the modulo of 'a' and 'b', further modulo 'c', is equal to the modulo of 'a' and 'c'. In other words, if a natural number 'c' is a divisor of 'b', the two-step modulus operation of 'a' by 'b' then by 'c' simplifies to a single modulus operation of 'a' by 'c'. This theorem can be useful when simplifying expressions involving modulus operations.
More concisely: If a natural number 'c' divides 'b', then for all natural number 'a', (a mod b) mod c = a mod c.
|
Nat.mul_dvd_mul
theorem Nat.mul_dvd_mul : ∀ {a b c d : ℕ}, a ∣ b → c ∣ d → a * c ∣ b * d
This theorem states that for any four natural numbers `a`, `b`, `c`, and `d`, if `a` divides `b` and `c` divides `d`, then the product of `a` and `c` divides the product of `b` and `d`. In mathematical notation, if $a | b$ and $c | d$, then $a \cdot c | b \cdot d$.
More concisely: If `a` divides `b` and `c` divides `d`, then `a * c` divides `b * d`.
|
Nat.le_of_dvd
theorem Nat.le_of_dvd : ∀ {m n : ℕ}, 0 < n → m ∣ n → m ≤ n
This theorem, `Nat.le_of_dvd`, states that for all natural numbers `m` and `n`, if `n` is greater than zero and `m` divides `n` (denoted by `m ∣ n`), then `m` is less than or equal to `n`. In simpler terms, any positive divisor of a natural number is always less than or equal to that number.
More concisely: For all natural numbers m and n, if n > 0 and m | n then m <= n.
|
Nat.eq_zero_of_zero_dvd
theorem Nat.eq_zero_of_zero_dvd : ∀ {a : ℕ}, 0 ∣ a → a = 0
This theorem states that for any natural number `a`, if `0` divides `a`, then `a` must be equal to `0`. In the language of number theory, if a number is divisible by zero, it must be zero itself.
More concisely: If 0 divides a natural number a, then a equals 0.
|
Nat.dvd_of_mul_dvd_mul_left
theorem Nat.dvd_of_mul_dvd_mul_left : ∀ {k m n : ℕ}, 0 < k → k * m ∣ k * n → m ∣ n
This theorem states that for any three natural numbers, `k`, `m`, and `n`, if `k` is greater than zero and `k` times `m` divides `k` times `n`, then `m` divides `n`. In mathematical notation, if $k > 0$ and $k \cdot m | k \cdot n$, then $m | n$. This theorem is crucial in arithmetic and number theory, as it establishes a relationship between multiplication and divisibility among natural numbers.
More concisely: If a positive natural number `k` divides the product of two other natural numbers `m` and `n` (i.e., `k * m` = `p * n` for some natural number `p`), then `m` divides `n` (i.e., `m` | `n`).
|
Nat.dvd_mul_right
theorem Nat.dvd_mul_right : ∀ (a b : ℕ), a ∣ a * b
This theorem states that for any two natural numbers `a` and `b`, `a` is a divisor of the product `a * b`. In mathematical terms, this is the principle that any number `a` divides its own multiplication with any other number `b`.
More concisely: For all natural numbers a and b, a divides the product a * b.
|
Nat.dvd_trans
theorem Nat.dvd_trans : ∀ {a b c : ℕ}, a ∣ b → b ∣ c → a ∣ c
This theorem states that for any three natural numbers `a`, `b`, and `c`, if `a` divides `b` and `b` divides `c`, then `a` also divides `c`. In mathematical notation, this would be expressed as: if $a | b$ and $b | c$, then $a | c$. This is a fundamental property of divisibility in the set of natural numbers.
More concisely: If `a` divides `b` and `b` divides `c`, then `a` divides `c` (in the set of natural numbers).
|
Nat.dvd_refl
theorem Nat.dvd_refl : ∀ (a : ℕ), a ∣ a
This theorem, `Nat.dvd_refl`, states that for any natural number `a`, `a` divides `a`. In the language of number theory, this is saying that any natural number is a divisor of itself. The symbol `∣` is used to represent the "divides" relation.
More concisely: For all natural numbers `a`, `a` divides `a`. In mathematical notation: ∀ (a : Nat), a | a.
|
Nat.dvd_zero
theorem Nat.dvd_zero : ∀ (a : ℕ), a ∣ 0
This theorem states that any natural number 'a' divides zero. In other words, for any given natural number, there exists another natural number such that when the former multiplies the latter, the result is zero. This is a standard property of division in mathematics represented in Lean 4.
More concisely: There exists a natural number that makes any natural number 'a' such that 'a * x = 0' holds in Lean 4. (This is the negative of the multiplicative identity for 'a', equivalent to 'a' dividing '0' in the context of Lean 4's natural numbers.)
|
Nat.dvd_add_iff_right
theorem Nat.dvd_add_iff_right : ∀ {k m n : ℕ}, k ∣ m → (k ∣ n ↔ k ∣ m + n)
This theorem states that for any three natural numbers 'k', 'm', and 'n', if 'k' divides 'm', then 'k' divides 'n' if and only if 'k' divides the sum of 'm' and 'n'. In the language of number theory, this is essentially asserting a property of divisibility and is particularly important when dealing with concepts like greatest common divisors and factorization.
More concisely: If k divides m and n, then k divides m + n. (This theorem is known as the Transitive Property of Divisibility or the Distributive Property of Divisibility.)
|
Nat.dvd_one
theorem Nat.dvd_one : ∀ {n : ℕ}, n ∣ 1 ↔ n = 1
This theorem states that for any natural number `n`, `n` divides 1 if and only if `n` is equal to 1. In terms of number theory, this means that 1 can only be divided evenly (i.e., without remainder) by the number 1 itself.
More concisely: For any natural number n, n divides 1 if and only if n = 1.
|
Nat.dvd_iff_mod_eq_zero
theorem Nat.dvd_iff_mod_eq_zero : ∀ (m n : ℕ), m ∣ n ↔ n % m = 0
This theorem states that for all natural numbers 'm' and 'n', 'm' divides 'n' if and only if the remainder of 'n' divided by 'm' is zero. In other words, it sets a condition for divisibility of one natural number by another. The condition is that when 'n' is divided by 'm', the modulus (remainder) should be zero. If this condition is met, then 'm' is a divisor of 'n' and vice versa.
More concisely: For natural numbers m and n, m divides n if and only if n mod m = 0.
|
Nat.div_mul_cancel
theorem Nat.div_mul_cancel : ∀ {n m : ℕ}, n ∣ m → m / n * n = m
This theorem states that for any two natural numbers `n` and `m`, if `n` divides `m` (denoted as `n ∣ m`), then dividing `m` by `n`, multiplying the result by `n`, we will get back `m`. This is a property of integer division, confirming that if a number `n` is a divisor of `m`, the 'div-then-multiply' operation on `m` with `n` will return `m`.
More concisely: If `n` divides `m` in Lean, then `m = n * (m ∝ n)`. (Here, `m ∝ n` denotes the quotient of `m` by `n` in Lean's integer division.)
|
Nat.mod_eq_zero_of_dvd
theorem Nat.mod_eq_zero_of_dvd : ∀ {m n : ℕ}, m ∣ n → n % m = 0
This theorem states that for any two natural numbers `m` and `n`, if `m` divides `n` (denoted as `m ∣ n`), then the remainder of `n` divided by `m` (`n % m`) is zero. Essentially, what this implies is that `n` is a multiple of `m` such that there is no remainder left when `n` is divided by `m`.
More concisely: If `m` divides `n`, then the remainder of `n` divided by `m` is zero. (i.e., `m ∣ n` implies `n % m = 0`).
|
Nat.dvd_add_iff_left
theorem Nat.dvd_add_iff_left : ∀ {k m n : ℕ}, k ∣ n → (k ∣ m ↔ k ∣ m + n)
This theorem states that for all natural numbers `k`, `m`, and `n`, if `k` divides `n`, then `k` divides `m` if and only if `k` divides `m + n`. In mathematical notation, this can be written as: ∀ k, m, n ∈ ℕ, if k | n, then k | m ⇔ k | (m + n).
More concisely: For all natural numbers `k`, `m`, and `n`, `k` divides `m` if and only if `k` divides `m + n`. (Or, equivalently, `k` | `m` ⇔ `k` | `(m + n)`.)
|
Nat.dvd_antisymm
theorem Nat.dvd_antisymm : ∀ {m n : ℕ}, m ∣ n → n ∣ m → m = n
This theorem, `Nat.dvd_antisymm`, states that for any two natural numbers `m` and `n`, if `m` divides `n` and `n` divides `m`, then `m` must be equal to `n`. In other words, if one natural number is a divisor of another and vice versa, the two numbers are the same. The divisibility relationship here is denoted by the `∣` symbol.
More concisely: If `m` divides `n` and `n` divides `m` in the natural numbers, then `m` equals `n`. (`m ∣ n` and `n ∣ m` imply `m = n`)
|
Nat.mul_div_assoc
theorem Nat.mul_div_assoc : ∀ {k n : ℕ} (m : ℕ), k ∣ n → m * n / k = m * (n / k)
This theorem states that for any natural numbers `k`, `n`, and `m`, if `k` divides `n`, then the result of first multiplying `m` and `n` and then dividing by `k` is equal to the result of first dividing `n` by `k` and then multiplying by `m`. In mathematical notation, this would be represented as: if $k | n$, then $m \cdot \frac{n}{k} = \frac{m \cdot n}{k}$.
More concisely: If `k` divides `n` in Lean, then `m * (n / k)` equals `(m * n) / k`.
|
Nat.mul_div_cancel'
theorem Nat.mul_div_cancel' : ∀ {n m : ℕ}, n ∣ m → n * (m / n) = m
This theorem states that for any two natural numbers `n` and `m`, if `n` divides `m` (denoted by `n ∣ m`), then the product of `n` and the quotient of `m` divided by `n` (expressed as `n * (m / n)`) equals `m`. Simply put, we multiply the divisor `n` with the result of integer division of `m` by `n`, and it equals the original dividend `m`. This matches with the concept in mathematics that when we divide a number by another and then multiply the result by the divisor, we should get back our initial number.
More concisely: For all natural numbers `n` and `m`, `n * (m / n) = m` when `n` divides `m`.
|
Nat.dvd_sub
theorem Nat.dvd_sub : ∀ {k m n : ℕ}, n ≤ m → k ∣ m → k ∣ n → k ∣ m - n
This theorem describes a property of divisibility among natural numbers. Specifically, it states that for any three natural numbers `k`, `m`, and `n`, if `n` is less than or equal to `m`, `k` divides `m` and `k` divides `n`, then `k` also divides the difference `m - n`.
More concisely: If `k` divides both `m` and `n` (`m ≥ n`), then `k` divides the difference `m - n`. (In mathematical notation: `k` | `m` and `k` | `n` imply `k` | `m - n`.)
|