Nat.mul_mod_right
theorem Nat.mul_mod_right : ∀ (m n : ℕ), m * n % m = 0
This theorem is stating that for any two natural numbers `m` and `n`, the remainder of the product of `m` and `n` divided by `m` is always zero. In other words, `m * n` is always a multiple of `m`, which is a basic property of integer multiplication and division.
More concisely: For all natural numbers m and n, m * n is a multiple of m.
|
Nat.div_eq_of_eq_mul_right
theorem Nat.div_eq_of_eq_mul_right : ∀ {n m k : ℕ}, 0 < n → m = n * k → m / n = k
This theorem is stating that for any three natural numbers `n`, `m`, and `k`, with `n` being greater than zero, if `m` is equal to the product of `n` and `k`, then the result of dividing `m` by `n` will be `k`. In mathematical terms, this theorem is stating that if $0 < n$ and $m = n \times k$, then $\frac{m}{n} = k$. This theorem essentially formalizes the fundamental property of division that if a number `m` is the product of `n` and `k`, dividing `m` by `n` will yield `k`.
More concisely: If $0 < n$ and $m = n \times k$, then $\frac{m}{n} = k$.
|
Nat.zero_div
theorem Nat.zero_div : ∀ (b : ℕ), 0 / b = 0
This theorem states that for any natural number `b`, the division of zero by `b` is zero. In mathematical terms, it simply states the well-known fact that zero divided by any natural number equals zero.
More concisely: For any natural number b, 0 divided by b equals 0.
|
Nat.mod_one
theorem Nat.mod_one : ∀ (x : ℕ), x % 1 = 0
This theorem states that for any natural number 'x', the remainder of 'x' divided by 1 is always 0. In mathematical notation, this is expressed as `x mod 1 = 0` for all natural numbers 'x'. This makes sense because dividing any number by 1 leaves no remainder.
More concisely: For all natural numbers x, the remainder of x divided by 1 is equal to zero. (x mod 1 = 0)
|
Nat.div_lt_iff_lt_mul
theorem Nat.div_lt_iff_lt_mul : ∀ {k x y : ℕ}, 0 < k → (x / k < y ↔ x < y * k)
This theorem states that for any natural numbers `k`, `x`, and `y`, with `k` being greater than zero, the condition of `x` divided by `k` being less than `y` is equivalent to the condition of `x` being less than `y` times `k`. In other words, determining whether one natural number divided by another is less than a third number is the same as determining whether the first number is less than the product of the third number and the divisor.
More concisely: For any natural numbers $k$, $x$, and $y$ with $k > 0$, $x / k < y$ if and only if $x < y \cdot k$.
|
Nat.div_le_self
theorem Nat.div_le_self : ∀ (n k : ℕ), n / k ≤ n
This theorem states that for any two natural numbers `n` and `k`, the result of integer division of `n` by `k` is always less than or equal to `n`. This is always true regardless of the values of `n` and `k` because integer division rounds down, so `n / k` is always going to be less than `n` unless `k` is 1.
More concisely: For all natural numbers n and k, ⌊n / k⌋ ≤ n. (Here, ⌊x⌋ denotes the floor function, which returns the largest integer less than or equal to x.)
|
Nat.div_eq_of_lt_le
theorem Nat.div_eq_of_lt_le : ∀ {k n m : ℕ}, k * n ≤ m → m < k.succ * n → m / n = k
This theorem states that for any three natural numbers `k`, `n`, and `m`, if `k * n` is less than or equal to `m` and `m` is strictly less than `(k+1) * n`, then the quotient of `m` divided by `n` is `k`. In other words, it provides a condition under which division of two natural numbers yields a specific quotient.
More concisely: If `k * n <= m` and `m < (k+1) * n`, then `m / n = k` as natural numbers.
|
Nat.zero_mod
theorem Nat.zero_mod : ∀ (b : ℕ), 0 % b = 0
This theorem states that for every natural number `b`, the modulus of 0 divided by `b` is 0. In other words, when zero is divided by any natural number, the remainder is always zero. This is consistent with the mathematical concept of division and modulus, where the modulus is the remainder left after division.
More concisely: For all natural numbers b, 0 mod b = 0.
|
Nat.mod_self
theorem Nat.mod_self : ∀ (n : ℕ), n % n = 0
This theorem states that for every natural number `n`, the remainder of `n` divided by itself is always `0`. In other words, any natural number `n` modulo `n` equals `0`. This corresponds to the mathematical concept that any number is exactly divisible by itself, leaving no remainder.
More concisely: For all natural numbers n, n mod n = 0.
|
Nat.mod_zero
theorem Nat.mod_zero : ∀ (a : ℕ), a % 0 = a
This theorem states that for any natural number `a`, the remainder of `a` divided by zero is `a` itself. In other words, if you try to divide any natural number by zero in Lean 4, instead of getting an error or undefined result, you get the original number back.
More concisely: The theorem asserts that for all natural numbers `a`, the remainder of `a` divided by zero, under any chosen residue class, is equal to `a`. (Note that this statement is not valid mathematically, as division by zero is undefined in standard mathematics. The behavior described in the theorem might be a defined property in the specific mathematical structure of Lean 4's natural numbers.)
|
Nat.add_div_right
theorem Nat.add_div_right : ∀ (x : ℕ) {z : ℕ}, 0 < z → (x + z) / z = (x / z).succ
This theorem states that for all natural numbers `x` and `z`, if `z` is greater than 0, then the division of the sum of `x` and `z` by `z` equals to the successor (or next natural number) of the result of the division of `x` by `z`. In mathematical terms, if `0 < z`, then `(x + z) / z = (x / z) + 1`.
More concisely: For any natural numbers `x` and `z` with `z > 0`, the quotient of the sum `x + z` by `z` equals the sum of the quotient of `x` by `z` and 1. In mathematical notation, `(x + z) / z = (x / z) + 1`.
|
Nat.mod_lt
theorem Nat.mod_lt : ∀ (x : ℕ) {y : ℕ}, y > 0 → x % y < y
This theorem states that for all natural numbers `x` and `y`, if `y` is greater than zero, then the modulus of `x` with respect to `y` (represented as `x % y`) is less than `y`. In mathematical terms, for any positive natural number `y`, the remainder of division of any natural number `x` by `y` is always less than `y`.
More concisely: For all natural numbers `x` and `y` with `y > 0`, `x % y` is less than `y`.
|
Nat.div_zero
theorem Nat.div_zero : ∀ (n : ℕ), n / 0 = 0
This theorem states that for any natural number `n`, the result of dividing `n` by zero is zero. This is a universal property that applies to all natural numbers. Please note that this is a convention in the Lean 4 theorem prover and might differ from other mathematical contexts where division by zero is usually undefined.
More concisely: For all natural numbers n, n divided by zero equals zero.
|
Nat.mul_div_left
theorem Nat.mul_div_left : ∀ (m : ℕ) {n : ℕ}, 0 < n → m * n / n = m
This theorem states that for any natural number `m` and any non-zero natural number `n`, the result of multiplying `m` and `n` then dividing by `n` is `m`. This essentially captures the principle that division is the inverse operation of multiplication for natural numbers. In more formal terms, the theorem states that for all `m` in the set of natural numbers, and for all `n` in the set of natural numbers excluding zero, `(m * n) / n` equals `m`.
More concisely: For all natural numbers `m` and non-zero `n`, `m * n = n * m` implies `m = (m * n) / n`.
|
Nat.div_mul_le_self
theorem Nat.div_mul_le_self : ∀ (m n : ℕ), m / n * n ≤ m
This theorem states that for all natural numbers `m` and `n`, the result of the integer division of `m` by `n` multiplied by `n` is always less than or equal to `m`. Essentially, it's asserting that the product of `n` and the floor division of `m` by `n` does not exceed `m`, which is a property of the floor division operation in mathematics.
More concisely: For all natural numbers m and n, m ÷ n × n ≤ m. (Here, ÷ denotes integer division.)
|
Nat.mod_eq_of_lt
theorem Nat.mod_eq_of_lt : ∀ {a b : ℕ}, a < b → a % b = a
This theorem states that for any two natural numbers `a` and `b`, if `a` is less than `b`, then the remainder when `a` is divided by `b` is `a` itself. In other words, for any two natural numbers, the modulo operation of the smaller number by the larger number results in the smaller number. This is because the division of a smaller number by a larger number in the set of natural numbers leads to a quotient of zero and a remainder equal to the smaller number.
More concisely: For all natural numbers `a` and `b` with `a < b`, `a % b = a`.
|
Nat.div_one
theorem Nat.div_one : ∀ (n : ℕ), n / 1 = n
This theorem states that for any natural number `n`, the quotient of `n` when divided by `1` is `n` itself. This is essentially an embodiment of the mathematical principle that any number divided by one remains the same.
More concisely: For all natural numbers n, n = n / 1.
|
Nat.mul_div_cancel
theorem Nat.mul_div_cancel : ∀ (m : ℕ) {n : ℕ}, 0 < n → m * n / n = m
This theorem states that for all natural numbers `m` and `n`, if `n` is greater than 0, then the result of multiplying `m` and `n` and then dividing by `n` is equal to `m`. This means that, within the set of natural numbers, multiplication and division by a non-zero number are inverse operations to each other.
More concisely: For all natural numbers m and n with n > 0, m * (1/n) = m.
|
Nat.mul_div_right
theorem Nat.mul_div_right : ∀ (n : ℕ) {m : ℕ}, 0 < m → m * n / m = n
This theorem states that for all natural numbers `n` and `m`, if `m` is greater than 0, then the result of multiplying `m` and `n` and then dividing the product by `m`, is equal to `n`. This is essentially a statement of the property of division that cancels the multiplication operation when the divisor is non-zero.
More concisely: For all natural numbers `n` and `m` (`m > 0`), `(m * n) / m = n`.
|
Nat.div_eq_of_eq_mul_left
theorem Nat.div_eq_of_eq_mul_left : ∀ {n m k : ℕ}, 0 < n → m = k * n → m / n = k
This theorem states that for any positive natural numbers `n`, `m`, and `k`, if `m` equals `k` multiplied by `n`, then the result of dividing `m` by `n` equals `k`. In other words, it captures the property of integers where division is the inverse operation of multiplication, provided the divisor is nonzero.
More concisely: For any natural numbers `n`, `m`, and `k`, if `m = k * n`, then `m / n = k`.
|
Nat.add_mul_mod_self_right
theorem Nat.add_mul_mod_self_right : ∀ (x y z : ℕ), (x + y * z) % z = x % z
This theorem states that for any three natural numbers `x`, `y`, and `z`, the remainder of the division of `x + y * z` by `z` is equal to the remainder of the division of `x` by `z`. In mathematical terms, it expresses the property `(x + yz) mod z = x mod z`.
More concisely: For any natural numbers x, y, and z, the remainder of (x + yz) divided by z is equal to the remainder of x divided by z.
|
Nat.le_div_iff_mul_le
theorem Nat.le_div_iff_mul_le : ∀ {k x y : ℕ}, 0 < k → (x ≤ y / k ↔ x * k ≤ y)
This theorem states that for any three natural numbers `k`, `x`, and `y`, where `k` is greater than zero, `x` is less than or equal to the integer division of `y` by `k` if and only if the product of `x` and `k` is less than or equal to `y`. In other words, for `k` > 0, `x` ≤ `y`/`k` is equivalent to `x`*`k` ≤ `y`.
More concisely: For natural numbers `k`, `x`, and `y` with `k` > 0, `x` leqs `y` divided by `k` is equivalent to `x` times `k` leqs `y`.
|
Nat.add_mod_right
theorem Nat.add_mod_right : ∀ (x z : ℕ), (x + z) % z = x % z
This theorem states that for any two natural numbers `x` and `z`, the result of the operation `(x + z) % z` is equal to `x % z`. In other words, adding a multiple of `z` (which is `x + z`) to `x` doesn't change the remainder when `x` is divided by `z`. This theorem reflects the property of modular arithmetic.
More concisely: For any natural numbers x and z, (x + z) % z = x % z.
|
Nat.add_mul_mod_self_left
theorem Nat.add_mul_mod_self_left : ∀ (x y z : ℕ), (x + y * z) % y = x % y
This theorem states that for all natural numbers `x`, `y`, and `z`, the remainder of the division of `(x + y * z)` by `y` is the same as the remainder of the division of `x` by `y`. In other words, adding a multiple of `y` to `x` doesn't change the remainder of `x` divided by `y`. This is a formulation of a property of modular arithmetic.
More concisely: For all natural numbers x, y, and z, (x + y \* z) mod y = x mod y.
|
Nat.mod_eq
theorem Nat.mod_eq : ∀ (x y : ℕ), x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x
This theorem states that for any two natural numbers `x` and `y`, the modulo of `x` with respect to `y` is equal to the modulo of the difference of `x` and `y` with respect to `y` if `y` is greater than 0 and less than or equal to `x`. Otherwise, the modulo of `x` with respect to `y` is `x` itself. Essentially, it describes how the modulo operation behaves with respect to subtraction and conditions on `y`.
More concisely: For all natural numbers x and y, if y > 0 and y <= x then x % y = (x - y) % y.
|
Nat.add_mul_div_right
theorem Nat.add_mul_div_right : ∀ (x y : ℕ) {z : ℕ}, 0 < z → (x + y * z) / z = x / z + y
This theorem states that for all natural numbers `x`, `y`, and `z`, given that `z` is greater than zero, the integer division of the sum of `x` and the product of `y` and `z` by `z` is equal to the sum of the integer division of `x` by `z` and `y`. This fits with the intuition that dividing a sum by a number distributes over the sum, at least when dealing with integer division where `z` is nonzero.
More concisely: For all natural numbers x, y, and z with z > 0, (x + y * z) / z = x / z + y.
|
Nat.mul_div_mul_left
theorem Nat.mul_div_mul_left : ∀ {m : ℕ} (n k : ℕ), 0 < m → m * n / (m * k) = n / k
This theorem states that for any positive integer `m` and any two arbitrary integers `n` and `k`, the result of dividing the product of `m` and `n` by the product of `m` and `k` is equal to the result of dividing `n` by `k`. In other words, for `m > 0, n, k ∈ ℕ`, we have `(m * n) / (m * k) = n / k`. This theorem is a property of integer division in the natural numbers.
More concisely: For any positive integers m, n, and k, the quotient of n by k is equal to the quotient of the product of m and n by the product of m and k. In other words, (m * n) / (m * k) = n / k.
|
Nat.mul_mod_mul_left
theorem Nat.mul_mod_mul_left : ∀ (z x y : ℕ), z * x % (z * y) = z * (x % y)
This theorem states that for any three natural numbers `z`, `x`, and `y`, the remainder of the product of `z` and `x` divided by the product of `z` and `y` is equal to the product of `z` and the remainder of `x` divided by `y`. In notation, we can write this as `z*x mod (z*y) = z*(x mod y)`. This is a property of the multiplication and modulus operations in the realm of natural numbers.
More concisely: For any natural numbers `z`, `x`, and `y`, `z*(x mod y)` equals `z*x mod (z*y)`.
|
Nat.div_div_eq_div_mul
theorem Nat.div_div_eq_div_mul : ∀ (m n k : ℕ), m / n / k = m / (n * k)
This theorem states that for any three natural numbers `m`, `n`, and `k`, the division of `m` by `n` followed by the division of the result by `k` is equal to the division of `m` by the product of `n` and `k`. In other words, `(m / n) / k = m / (n * k)` for all natural numbers `m`, `n`, and `k`.
More concisely: For all natural numbers m, n, and k, (m / n) / k = m / (n * k).
|
Nat.mul_mod_left
theorem Nat.mul_mod_left : ∀ (m n : ℕ), m * n % n = 0
This theorem states that for all natural numbers `m` and `n`, the remainder of the product of `m` and `n` divided by `n` is always `0`. In mathematical terms, this says `m*n mod n = 0` for all `m`,`n` in the set of natural numbers. This is consistent with the property of modulus operation, the remainder of any number `x` divided by `y` is zero if `x` is a multiple of `y`, and `m*n` is clearly a multiple of `n`.
More concisely: For all natural numbers m and n, m * n is a multiple of n.
|
Nat.add_mod_left
theorem Nat.add_mod_left : ∀ (x z : ℕ), (x + z) % x = z % x
This theorem, `Nat.add_mod_left`, states that for all natural numbers 'x' and 'z', the modulus of the sum of 'x' and 'z' with respect to 'x' is equal to the modulus of 'z' with respect to 'x'. In simple terms, adding 'x' to 'z' doesn't change the remainder when 'z' is divided by 'x'. This theorem represents a fundamental property of modular arithmetic.
More concisely: For all natural numbers x and z, x | (z + x) if and only if x | z. (x being a divisor of z + x if and only if x being a divisor of z in the context of modular arithmetic)
|
Nat.div_add_mod
theorem Nat.div_add_mod : ∀ (m n : ℕ), n * (m / n) + m % n = m
This theorem states that for any two natural numbers `m` and `n`, the sum of `n` times the quotient of `m` divided by `n` and the remainder of `m` divided by `n` is equal to `m`. This is a formalization of the "division algorithm", or Euclidean division, which states that for any two positive integers `m` and `n`, there exist unique integers `q` and `r` such that `m = n*q + r` and `0 ≤ r < |n|`, where `q` is the quotient and `r` is the remainder.
More concisely: For any natural numbers `m` and `n`, `m` equals the sum of `n` times the quotient of `m` by `n` and the remainder of `m` divided by `n`.
|
Nat.mod_add_div
theorem Nat.mod_add_div : ∀ (m k : ℕ), m % k + k * (m / k) = m
This theorem states that for all natural numbers `m` and `k`, the modulus of `m` by `k` added to `k` times the integer division of `m` by `k` equals `m`. In other words, if you divide `m` by `k`, multiply the quotient by `k`, and then add the remainder, you get back the original number `m`. This is a formalization of the Euclidean division algorithm in the natural numbers.
More concisely: For all natural numbers m and k, m = k * (m div k) + m mod k.
|
Nat.div_lt_self
theorem Nat.div_lt_self : ∀ {n k : ℕ}, 0 < n → 1 < k → n / k < n
This theorem states that for every pair of natural numbers `n` and `k`, if `n` is greater than zero and `k` is greater than one, then the integer division of `n` by `k` is less than `n`. In other words, dividing a positive natural number by another natural number greater than one results in a number which is less than the original number.
More concisely: For all natural numbers `n` greater than zero and `k` greater than one, `n` > `k` > 0 implies `n` / `k` < `n`.
|
Nat.add_mul_div_left
theorem Nat.add_mul_div_left : ∀ (x z : ℕ) {y : ℕ}, 0 < y → (x + y * z) / y = x / y + z
This theorem states that for any natural numbers `x` and `z` and for any non zero natural number `y`, the division of the sum of `x` and the product of `y` and `z` by `y` is equal to the sum of the division of `x` by `y` and `z`. In terms of mathematical notation, it asserts that $\frac{x + yz}{y} = \frac{x}{y} + z$ when $y > 0$.
More concisely: For any natural numbers x, y (with y > 0), and z, the quotient of x + yz by y is equal to the sum of the quotient of x by y and z. In mathematical notation: $\frac{x + yz}{y} = \frac{x}{y} + z$.
|
Nat.mul_div_le
theorem Nat.mul_div_le : ∀ (m n : ℕ), n * (m / n) ≤ m
This theorem states that for all natural numbers `m` and `n`, the product of `n` and the quotient of `m` divided by `n` is less than or equal to `m`. In mathematical terms, for all `m, n ∈ ℕ`, we have `n * (m / n) ≤ m`. This basically encapsulates the property of integer division, where the product of the divisor and the quotient is less than or equal to the dividend.
More concisely: For all natural numbers `m` and `n`, `n * (m ÷ n) ≤ m`. (Here `÷` represents integer division in Lean 4.)
|
Nat.div_self
theorem Nat.div_self : ∀ {n : ℕ}, 0 < n → n / n = 1
This theorem states that for any natural number 'n', if 'n' is greater than zero, then the result of dividing 'n' by itself is 1. Put simply, it formalizes the common mathematical fact that any non-zero number divided by itself equals one.
More concisely: For any natural number n greater than zero, n / n = 1.
|
Nat.div_eq
theorem Nat.div_eq : ∀ (x y : ℕ), x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0
This theorem expresses how division is calculated for two natural numbers `x` and `y`. If `y` is positive and less than or equal to `x`, then the quotient of `x / y` is computed by subtracting `y` from `x`, performing the division of the result by `y`, and then adding one. If `y` is not positive or is greater than `x`, then the quotient of `x / y` is simply zero. In essence, this theorem captures the core behavior of integer division in mathematics.
More concisely: For natural numbers `x` and `y` with `y > 0` and `y <= x`, the quotient `x / y` equals `(x - y) / y + 1`. Otherwise, `x / y` equals 0.
|
Nat.mul_div_cancel_left
theorem Nat.mul_div_cancel_left : ∀ (m : ℕ) {n : ℕ}, 0 < n → n * m / n = m
This theorem states that for any two natural numbers `m` and `n`, where `n` is greater than zero, if you multiply `n` and `m` together and then divide the result by `n`, you will get back `m`. It essentially asserts the fundamental property of division and multiplication being inverse operations with respect to each other, in the context of natural numbers.
More concisely: For all natural numbers `m` and `n` (`n` > 0), `m * (1 / n) = n * m`.
|
Nat.mod_eq_sub_mod
theorem Nat.mod_eq_sub_mod : ∀ {a b : ℕ}, a ≥ b → a % b = (a - b) % b
This theorem states that for any two natural numbers `a` and `b`, if `a` is greater than or equal to `b`, then the remainder of `a` divided by `b` is equal to the remainder of the difference of `a` and `b` divided by `b`. In mathematical notation, for all $a, b \in \mathbb{N}$ such that $a \geq b$, we have $a \mod b = (a - b) \mod b$.
More concisely: For all natural numbers `a` and `b` with `a >= b`, the remainder of `a` divided by `b` equals the remainder of `(a - b)` divided by `b`.
|
Nat.mod_le
theorem Nat.mod_le : ∀ (x y : ℕ), x % y ≤ x
This theorem states that for all natural numbers `x` and `y`, the remainder of `x` divided by `y` (expressed as `x % y`) is always less than or equal to `x`. In other words, when a natural number is divided by any other natural number, the remainder of the division operation can never be more than the dividend.
More concisely: For all natural numbers x and y, x % y ≤ x.
|
Nat.div_eq_of_lt
theorem Nat.div_eq_of_lt : ∀ {a b : ℕ}, a < b → a / b = 0
This theorem states that for any two natural numbers 'a' and 'b', if 'a' is less than 'b', then the result of dividing 'a' by 'b' is zero. This is based on the property of integer division where the quotient of a division operation between two natural numbers is zero if the dividend is less than the divisor.
More concisely: For all natural numbers a and b, if a < b then (a / b) = 0.
|