Nat.mul_eq_zero
theorem Nat.mul_eq_zero : ∀ {m n : ℕ}, n * m = 0 ↔ n = 0 ∨ m = 0
This theorem states that for any two natural numbers `m` and `n`, the multiplication of `n` and `m` equals zero if and only if either `n` or `m` is zero. In other words, in the realm of natural numbers, zero is the only number which, when multiplied by another number, yields zero.
More concisely: For all natural numbers m and n, m * n = 0 if and only if m = 0 or n = 0.
|
Nat.mul_ne_zero_iff
theorem Nat.mul_ne_zero_iff : ∀ {n m : ℕ}, n * m ≠ 0 ↔ n ≠ 0 ∧ m ≠ 0
This theorem states that for any two natural numbers `n` and `m`, the product of `n` and `m` is not zero if and only if both `n` and `m` are not zero. In other words, the only way the multiplication of two natural numbers can result in zero is if at least one of the numbers is zero itself.
More concisely: For natural numbers `n` and `m`, `n * m = 0` if and only if `n = 0` or `m = 0`.
|
Nat.mod_two_eq_zero_or_one
theorem Nat.mod_two_eq_zero_or_one : ∀ (n : ℕ), n % 2 = 0 ∨ n % 2 = 1
This theorem states that for any natural number `n`, the remainder when `n` is divided by 2 is either 0 or 1. This is equivalent to saying that any natural number is either even (divisible by 2) or odd (leaves a remainder of 1 when divided by 2).
More concisely: For any natural number n, the remainder of n when divided by 2 is either 0 or 1. (Equivalently, every natural number is either even or odd.)
|
Nat.div_eq_iff_eq_mul_left
theorem Nat.div_eq_iff_eq_mul_left : ∀ {a b c : ℕ}, 0 < b → b ∣ a → (a / b = c ↔ a = c * b)
This theorem states that for any natural numbers `a`, `b`, and `c`, given that `b` is not zero and `b` divides `a`, the quotient of `a` divided by `b` is equal to `c` if and only if `a` is equal to `c` multiplied by `b`. This theorem provides a relationship between division and multiplication in the context of natural numbers.
More concisely: For natural numbers `a`, `b`, and `c`, `a = c * b` if and only if `b` non-zero and `b` divides `a`, resulting in `a / b = c`.
|
Nat.succ_add_eq_add_succ
theorem Nat.succ_add_eq_add_succ : ∀ (a b : ℕ), a.succ + b = a + b.succ
This theorem states that for any two natural numbers `a` and `b`, the successor of `a` plus `b` is equal to `a` plus the successor of `b`. In terms of traditional mathematics, if `a` and `b` are natural numbers, then `(a+1) + b = a + (b+1)`. This theorem encapsulates a fundamental property of addition, which is commutativity of incrementation.
More concisely: For any natural numbers `a` and `b`, `(a + 1) + b = a + (b + 1)`.
|
Nat.sub_one
theorem Nat.sub_one : ∀ (n : ℕ), n - 1 = n.pred
This theorem states that for any natural number 'n', subtracting one from 'n' is equal to applying the predecessor function on 'n'. In other words, for all natural numbers 'n', 'n - 1' is equivalent to the result of the 'Nat.pred' function when given 'n' as an argument. The predecessor function returns 'n - 1' for any given natural number 'n', but if 'n' is zero, it returns zero.
More concisely: For all natural numbers n, Nat.pred n = n - 1.
|
Nat.one_le_two_pow
theorem Nat.one_le_two_pow : ∀ {n : ℕ}, 1 ≤ 2 ^ n
This theorem states that for any non-negative integer `n`, the value of `1` is less than or equal to `2` raised to the power of `n`. This is because any power of `2` is always at least `1`, since `2` to the power of `0` is `1` and for `n > 0`, `2` to the power of `n` is always more than `1`.
More concisely: For all non-negative integers n, 1 ≤ 2^n.
|
Nat.lt_of_add_lt_add_left
theorem Nat.lt_of_add_lt_add_left : ∀ {k m n : ℕ}, n + k < n + m → k < m
This theorem states that for all natural numbers `k`, `m`, and `n`, if `n + k` is less than `n + m`, then `k` is less than `m`. Essentially, it uses the property of addition to compare two natural numbers: if adding the same number `n` to two numbers `k` and `m` results in a smaller sum for `k`, then `k` must be smaller than `m`.
More concisely: For all natural numbers `k` and `m`, if `n + k` < `n + m`, then `k` < `m`.
|
Nat.pow_lt_pow_of_lt
theorem Nat.pow_lt_pow_of_lt : ∀ {a n m : ℕ}, 1 < a → n < m → a ^ n < a ^ m
This theorem states that for any natural numbers `a`, `n`, and `m`, if `a` is greater than 1 and `n` is less than `m`, then `a` raised to the power `n` is less than `a` raised to the power `m`. In other words, for positive natural numbers, raising a larger base to a power results in a greater number, and similarly, raising a base to a larger exponent also results in a greater number.
More concisely: For all natural numbers `a`, `n`, and `m` where `a` is greater than 1 and `n` is less than `m`, the inequality `a^n < a^m` holds.
|
Nat.add_sub_cancel'
theorem Nat.add_sub_cancel' : ∀ {n m : ℕ}, m ≤ n → m + (n - m) = n
This theorem, `Nat.add_sub_cancel'`, states that for all natural numbers `n` and `m`, if `m` is less than or equal to `n`, then adding `m` to the difference of `n` and `m` will yield `n`. Essentially, this is saying that we can "cancel out" the subtraction by adding the subtracted element back, assuming the natural number we are subtracting is less than or equal to the original number. This theorem is a specific instance of the general algebraic property that `n = m + (n - m)` when `m ≤ n`.
More concisely: For all natural numbers `n` and `m` with `m <= n`, `n = (n - m) + m`.
|
Nat.pow_dvd_pow_iff_le_right
theorem Nat.pow_dvd_pow_iff_le_right : ∀ {x k l : ℕ}, 1 < x → (x ^ k ∣ x ^ l ↔ k ≤ l)
This theorem states that for any natural numbers `x`, `k`, and `l`, if `x` is greater than 1, then `x` raised to the power of `k` divides `x` raised to the power of `l` if and only if `k` is less than or equal to `l`.
More concisely: For any natural numbers x, k, and l, x^k divides x^l if and only if k <= l.
|
Nat.zero_max
theorem Nat.zero_max : ∀ (a : ℕ), max 0 a = a
This theorem states that for any natural number `a`, the maximum value between 0 and `a` is `a` itself. In other words, no matter what natural number you choose, it will always be greater than or equal to zero. Therefore, when you use the `max` function to compare zero with any natural number, the result will always be that natural number.
More concisely: For any natural number `a`, 0 ≤ a holds, thus max 0 a = a.
|
Nat.mul_lt_mul_of_lt_of_le'
theorem Nat.mul_lt_mul_of_lt_of_le' : ∀ {a c b d : ℕ}, a < c → b ≤ d → 0 < b → a * b < c * d
This theorem states that for any four natural numbers `a`, `c`, `b`, and `d`, if `a` is less than `c`, `b` is less than or equal to `d`, and `b` is greater than 0, then the product of `a` and `b` is less than the product of `c` and `d`. In other words, under these conditions, multiplying a smaller natural number by another natural number yields a result that is less than the product of two larger or equal natural numbers. This theorem is a special case of the more general principle that multiplication preserves the order of natural numbers.
More concisely: If `a` < `c` and `b` > 0 and `b` <= `d`, then `a * b` < `c * d`.
|
Nat.mul_ne_zero
theorem Nat.mul_ne_zero : ∀ {n m : ℕ}, n ≠ 0 → m ≠ 0 → n * m ≠ 0
This theorem states that for any two natural numbers `n` and `m`, if neither `n` nor `m` are zero, then their product `n * m` is also not zero. It emphasizes the fact that the multiplication of two non-zero natural numbers will never result in zero.
More concisely: If two natural numbers are non-zero, their product is also non-zero.
|
Nat.pow_pos
theorem Nat.pow_pos : ∀ {a n : ℕ}, 0 < a → 0 < a ^ n
This theorem states that for any natural numbers `a` and `n`, if `a` is greater than 0, then `a` raised to the power of `n` (denoted as `a ^ n`) is also greater than 0. In mathematical terms, it asserts that for any positive natural number `a`, the nth power of `a` is always positive for any natural number `n`.
More concisely: For any positive natural number `a` and natural number `n`, `a^n` is also a positive natural number.
|
Nat.mod_mod
theorem Nat.mod_mod : ∀ (a n : ℕ), a % n % n = a % n
This theorem states that for any two natural numbers 'a' and 'n', taking the modulus of 'a' with 'n' twice in succession is equal to taking the modulus just once. In other words, if you calculate 'a' % 'n' and then apply the modulus operation with 'n' again, the result will be the same as 'a' % 'n'. This is represented in Lean 4 as `a % n % n = a % n`.
More concisely: For all natural numbers a and n, the repeated modulus operation a % n % n equals the single modulus operation a % n.
|
Nat.mul_add_mod
theorem Nat.mul_add_mod : ∀ (m x y : ℕ), (m * x + y) % m = y % m
This theorem states that for any three natural numbers `m`, `x`, and `y`, the modulus of the sum of `m` multiplied by `x` and `y` with respect to `m` is equal to the modulus of `y` with respect to `m`. In other words, the remainder of dividing `(m * x + y)` by `m` is the same as the remainder of dividing `y` by `m`. This is an important property of modular arithmetic.
More concisely: For any natural numbers `m`, `x`, and `y`, `(m * x + y) % m = y % m`.
|
Nat.max_zero
theorem Nat.max_zero : ∀ (a : ℕ), max a 0 = a
This theorem states that for any natural number `a`, the maximum of `a` and `0` is always `a`. In other words, when you compare any natural number with zero and you take the larger one, you always get the natural number itself, as all natural numbers are greater than or equal to zero.
More concisely: For all natural numbers `a`, `a` is greater than or equal to 0, so `max 0 a = a`.
|
Nat.mul_mod
theorem Nat.mul_mod : ∀ (a b n : ℕ), a * b % n = a % n * (b % n) % n
This theorem is stating a property of multiplication and modulus in the context of natural numbers. Specifically, for any three natural numbers `a`, `b`, and `n`, the result of multiplying `a` and `b`, and then taking the modulus of the result with respect to `n`, is equivalent to first taking the modulus of `a` and `b` with respect to `n`, multiplying these results, and then taking the modulus of this result with respect to `n` once again. This can be mathematically represented as `(a * b) mod n = ((a mod n) * (b mod n)) mod n`.
More concisely: For any natural numbers `a`, `b`, and `n`, `(a * b) mod n` equals `((a mod n) * (b mod n)) mod n`.
|
Nat.pow_succ'
theorem Nat.pow_succ' : ∀ {m n : ℕ}, m ^ n.succ = m * m ^ n
This theorem states that for any natural numbers `m` and `n`, the power of `m` to the successor of `n` (or `m` to the power of `n + 1`) is equal to `m` multiplied by `m` to the power of `n`. In mathematical notation, this theorem states that $m^{n+1} = m * m^n$.
More concisely: The theorem asserts that for any natural number `m` and `n`, `m^(n+1)` equals `m * m^n`.
|
Nat.min_self
theorem Nat.min_self : ∀ (a : ℕ), min a a = a
This theorem states that for every natural number `a`, the minimum of `a` and `a` is always `a` itself. The minimum function `min` is used to determine the lesser of two values. In this case, since the two values are the same, the result is always that value.
More concisely: For all natural numbers a, a is the minimum value of a and a.
|
Nat.zero_min
theorem Nat.zero_min : ∀ (a : ℕ), min 0 a = 0
This theorem states that for any natural number `a`, the minimum value between `0` and `a` is `0`. In other words, when you compare zero with any natural number using the `min` function, the result will always be zero.
More concisely: For any natural number `a`, `0` is the minimum value. (or)
The minimum value of `0` and any natural number `a` is `0`.
|
Nat.max_eq_right
theorem Nat.max_eq_right : ∀ {a b : ℕ}, a ≤ b → max a b = b
This theorem, `Nat.max_eq_right`, states that for any two natural numbers `a` and `b`, if `a` is less than or equal to `b`, then the maximum value between `a` and `b` is `b`. Essentially, if `b` is greater than or equal to `a`, then `b` is considered the maximum of the two numbers.
More concisely: For all natural numbers a and b, if a ≤ b then max a b = b.
|
Nat.sub_sub_self
theorem Nat.sub_sub_self : ∀ {n m : ℕ}, m ≤ n → n - (n - m) = m
This theorem, `Nat.sub_sub_self`, states that for any two natural numbers `n` and `m`, if `m` is less than or equal to `n`, then subtracting `m` from `n` and then subtracting the result from `n` equals `m`. In mathematical notation, this theorem is expressing the formula `n - (n - m) = m` for `n ≥ m`. This theorem gives us an important property of subtraction for natural numbers.
More concisely: For any natural numbers `n` and `m` with `m ≤ n`, we have `n = (n - m) + m`.
|
Nat.succ_max_succ
theorem Nat.succ_max_succ : ∀ (x y : ℕ), max x.succ y.succ = (max x y).succ
This theorem states that for any two natural numbers `x` and `y`, the maximum of their successors (i.e., `x + 1` and `y + 1`) is the successor of the maximum of `x` and `y`. In other words, adding one to both numbers before finding the maximum yields the same result as finding the maximum first and then adding one.
More concisely: For all natural numbers x and y, (x + 1)max (y + 1) = (x max y) + 1.
|
Nat.pow_one
theorem Nat.pow_one : ∀ (a : ℕ), a ^ 1 = a
This theorem states that for any natural number 'a', 'a' raised to the power of 1 is equal to 'a' itself. In other words, the first power of any natural number is the number itself.
More concisely: For all natural numbers a, a^1 = a.
|
Nat.exists_eq_add_of_lt
theorem Nat.exists_eq_add_of_lt : ∀ {m n : ℕ}, m < n → ∃ k, n = m + k + 1
This theorem states that for any two natural numbers `m` and `n`, if `m` is less than `n`, then there exists a natural number `k` such that `n` is equal to `m + k + 1`. In other words, if one natural number is smaller than another, you can find some natural number that when added to the smaller number and one, gives you the larger number.
More concisely: For any natural numbers `m` and `n` with `m < n`, there exists a natural number `k` such that `n = m + k + 1`.
|
Nat.pow_add
theorem Nat.pow_add : ∀ (a m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
This theorem, `Nat.pow_add`, states that for all natural numbers `a`, `m`, and `n`, the power of `a` raised to the sum of `m` and `n` is equal to the product of `a` raised to the power `m` and `a` raised to the power `n`. This is an important property in mathematics often referred to as the rule of exponents, specifically, the multiplication rule, which in this case, is applied to natural numbers. In mathematical notation, this theorem can be expressed as a^(m + n) = a^m * a^n.
More concisely: For all natural numbers `a`, `m`, and `n`, `a^(m + n)` equals the product `a^m * a^n`.
|
Nat.lt_add_of_pos_left
theorem Nat.lt_add_of_pos_left : ∀ {k n : ℕ}, 0 < k → n < k + n
This theorem, `Nat.lt_add_of_pos_left`, states that for any two natural numbers `k` and `n`, if `k` is greater than zero, then `n` is less than the sum of `k` and `n`. In other words, if you have a positive natural number `k`, adding it to any other natural number `n` will result in a number that is strictly larger than `n`.
More concisely: For all natural numbers `k` and `n`, if `k > 0` then `n < k + n`.
|
Nat.add_mod
theorem Nat.add_mod : ∀ (a b n : ℕ), (a + b) % n = (a % n + b % n) % n
This theorem in Lean 4 states that for any three natural numbers a, b, and n, the modulus of the sum of a and b with respect to n is equal to the modulus of the sum of the modulus of a with respect to n and the modulus of b with respect to n, again taken modulus n. In terms of mathematical notation, it asserts that for all a, b, and n in the set of natural numbers, (a + b) mod n = ((a mod n) + (b mod n)) mod n. This theorem is essentially a formal statement of one of the properties of modular arithmetic.
More concisely: For all natural numbers a, b, and n, (a + b) % n = (a % n + b % n) % n, where % denotes modulo operation.
|
Nat.sub_add_comm
theorem Nat.sub_add_comm : ∀ {n m k : ℕ}, k ≤ n → n + m - k = n - k + m
This theorem, `Nat.sub_add_comm`, states that for any three natural numbers `n`, `m`, and `k`, if `k` is less than or equal to `n`, then adding `m` to `n` and then subtracting `k` is the same as subtracting `k` from `n` first and then adding `m`. In mathematical notation, this is stating that if $k \leq n$, then $n + m - k = n - k + m$.
More concisely: For all natural numbers $n$, $m$, and $k$ with $k \leq n$, we have $n + m = n + m - k + k = n - k + m$.
|
Nat.add_lt_of_lt_sub'
theorem Nat.add_lt_of_lt_sub' : ∀ {a b c : ℕ}, b < c - a → a + b < c
This theorem states that for all natural numbers `a`, `b`, and `c`, if `b` is less than the difference of `c` and `a`, then the sum of `a` and `b` is less than `c`. Essentially, this means that if you subtract `a` from `c` and the result is greater than `b`, then when you add `a` and `b` together, the result will be less than `c`. This theorem captures a specific relationship between the operations of addition and subtraction in the context of natural numbers.
More concisely: For all natural numbers `a`, `b`, and `c`, if `b` < `c` - `a`, then `a` + `b` < `c`.
|
Nat.eq_mul_of_div_eq_right
theorem Nat.eq_mul_of_div_eq_right : ∀ {a b c : ℕ}, b ∣ a → a / b = c → a = b * c
This theorem states that for any three natural numbers `a`, `b`, and `c`, if `b` divides `a` and the result of dividing `a` by `b` is `c`, then `a` is equal to the product of `b` and `c`. In other words, it formalizes the arithmetic property that if a number `a` is evenly divisible by `b` yielding a quotient `c`, then `a` can also be represented by the multiplication of `b` and `c`.
More concisely: If `a` is divisible by `b` with remainder `c`, then `a` equals `b` times `c`.
|
Nat.succ_min_succ
theorem Nat.succ_min_succ : ∀ (x y : ℕ), min x.succ y.succ = (min x y).succ
This theorem states that for every pair of natural numbers 'x' and 'y', the minimum of the successors of 'x' and 'y' (i.e., 'x+1' and 'y+1') is equal to the successor (i.e., plus one) of the minimum of 'x' and 'y'. In other words, incrementing both numbers and then taking the minimum yields the same result as first taking the minimum and then incrementing.
More concisely: For all natural numbers x and y, x.succ min x y = y.succ min x y.
|
Nat.mul_lt_mul_of_le_of_lt
theorem Nat.mul_lt_mul_of_le_of_lt : ∀ {a c b d : ℕ}, a ≤ c → b < d → 0 < c → a * b < c * d
This theorem states that for any four natural numbers `a`, `b`, `c`, and `d`, if `a` is less than or equal to `c`, `b` is less than `d`, and `c` is greater than 0, then the product of `a` and `b` is less than the product of `c` and `d`. This theorem represents a basic inequality property of multiplication in the natural numbers.
More concisely: If a ≤ c and b < d, then a * b < c * d.
|
Nat.shiftRight_succ_inside
theorem Nat.shiftRight_succ_inside : ∀ (m n : ℕ), m >>> (n + 1) = (m / 2) >>> n
This theorem, named `Nat.shiftRight_succ_inside`, states that for all natural numbers `m` and `n`, shifting `m` right by `n + 1` places is equivalent to first dividing `m` by 2 and then shifting the result right by `n` places. In other words, you can move the operation of dividing by 2 inside the shift right operation without changing the result. This is a property of binary shift operations on natural numbers in Lean 4.
More concisely: For all natural numbers m and n, (m >>< (n + 1)) = (shift_right m n) /~ 2^(n+1) where >>< denotes right shift and /~ denotes unsigned division in Lean 4.
|
Nat.one_lt_two_pow
theorem Nat.one_lt_two_pow : ∀ {n : ℕ}, n ≠ 0 → 1 < 2 ^ n
This theorem states that for all non-zero natural numbers `n`, 1 is less than 2 raised to the power of `n`. In other words, any power of 2 (where the exponent is a non-zero natural number) is always greater than 1.
More concisely: For all non-zero natural numbers n, 2^n > 1.
|
Nat.add_le_of_le_sub'
theorem Nat.add_le_of_le_sub' : ∀ {n k m : ℕ}, m ≤ k → n ≤ k - m → m + n ≤ k
This theorem states that for any three natural numbers `n`, `k`, and `m`, if `m` is less than or equal to `k` and `n` is less than or equal to the difference of `k` and `m`, then the sum of `m` and `n` is less than or equal to `k`. In other words, if we subtract a certain amount from a number and the remaining value is still larger than or equal to another number, then the sum of the subtracted amount and the other number will not exceed the original number.
More concisely: If `m` is less than or equal to `k` and `n` is less than or equal to `k - m`, then `m + n` is less than or equal to `k`.
|
Nat.shiftLeft_succ_inside
theorem Nat.shiftLeft_succ_inside : ∀ (m n : ℕ), m <<< (n + 1) = (2 * m) <<< n
This theorem is stating that for all natural numbers `m` and `n`, shifting `m` to the left by `(n + 1)` places is equivalent to doubling `m` and then shifting the result to the left by `n` places. Here, the notation `<<<` denotes a left bit shift in binary representation, which is akin to performing multiplication by powers of 2. The theorem thus gives a property that relates the shift operation on a number and its successor.
More concisely: For all natural numbers m and n, shifting m left by (n + 1) places is equivalent to doubling m and then shifting the result left by n places. In other words, m <<< (n + 1) = 2^n * m <<< n.
|
Nat.succ_eq_one_add
theorem Nat.succ_eq_one_add : ∀ (n : ℕ), n.succ = 1 + n
This theorem states that for any natural number `n`, the successor of `n` (denoted as `Nat.succ n`) is equal to `1 + n`. In other words, it asserts that the operation of finding the next natural number (successor operation) is equivalent to adding one to the given natural number. This is a foundational aspect of the arithmetic of natural numbers.
More concisely: For all natural numbers n, Nat.succ n equals 1 + n.
|
Nat.add_one_sub_one
theorem Nat.add_one_sub_one : ∀ (n : ℕ), n + 1 - 1 = n
This theorem states that for any natural number `n`, if you add 1 to `n` and then subtract 1, you will get `n` back. In other words, the operations of adding 1 and subtracting 1 on a natural number cancel each other out, leaving the original number unchanged. This is expressed formally in Lean 4 as `n + 1 - 1 = n` for all natural numbers `n`.
More concisely: For all natural numbers `n`, the operation of adding 1 and then subtracting 1 is equal to the identity function, that is, `n + 1 - 1 = n`.
|
Nat.zero_shiftRight
theorem Nat.zero_shiftRight : ∀ (n : ℕ), 0 >>> n = 0
This theorem states that for any natural number `n`, right-shifting zero `n` places results in zero. In other words, in the context of bit manipulation, if you take the number zero and shift its bits to the right `n` times, the result will always be zero, regardless of the value of `n`.
More concisely: For any natural number `n`, right-shifting the binary representation of zero `n` times results in zero.
|
Nat.le_mul_of_pos_left
theorem Nat.le_mul_of_pos_left : ∀ {n : ℕ} (m : ℕ), 0 < n → m ≤ n * m
This theorem states that for any natural numbers `n` and `m`, if `n` is greater than 0, then `m` is less than or equal to the product of `n` and `m`. Essentially, this means that for any non-zero natural number `n`, multiplying it with another natural number `m` (which could be zero) can never result in a value smaller than `m`.
More concisely: For all natural numbers n and m, if n > 0 then m <= n * m.
|
Nat.min_zero
theorem Nat.min_zero : ∀ (a : ℕ), min a 0 = 0
This theorem states that for any natural number `a`, the minimum of `a` and `0` is `0`. In other words, zero is less than or equal to every natural number, so when comparing zero with any natural number, zero is always the minimum.
More concisely: For all natural numbers `a`, `0 ≤ a`. (Zero is less than or equal to every natural number.)
|
Nat.mod_add_mod
theorem Nat.mod_add_mod : ∀ (m n k : ℕ), (m % n + k) % n = (m + k) % n
This theorem states that for any three natural numbers `m`, `n`, and `k`, the remainder left when `m` is divided by `n` added to `k` and then the result divided by `n` is equal to the remainder when `m` plus `k` is divided by `n`. In other words, the modulo operation distributes over addition. The theorem is given by the expression `(m % n + k) % n = (m + k) % n`, where `%` denotes the modulo operation.
More concisely: For any natural numbers `m`, `n`, and `k`, `(m % n + k) % n = (m + k) % n` holds true for the modulo operation.
|
Nat.one_add
theorem Nat.one_add : ∀ (n : ℕ), 1 + n = n.succ
This theorem states that for any natural number `n`, the sum of `1` and `n` is equal to the successor of `n`. In more mathematical terms, the theorem is saying that for all natural numbers `n`, 1 + n = n + 1, where "succ" denotes the successor function (i.e., the function that gives the next natural number). This corresponds to the intuitive concept of adding one to a number to get the next number.
More concisely: For all natural numbers `n`, `1 + n = succ(n)`.
|
Nat.sub_min_sub_right
theorem Nat.sub_min_sub_right : ∀ (a b c : ℕ), min (a - c) (b - c) = min a b - c
This theorem states that for any three natural numbers `a`, `b`, and `c`, the minimum of the difference between `a` and `c` and the difference between `b` and `c` is equal to the difference between the minimum of `a` and `b` and `c`. In other words, when subtracting `c` from both `a` and `b`, taking the minimum before or after the subtraction yields the same result.
More concisely: For any natural numbers `a`, `b`, and `c`, `min (a - c) (b - c)` equals `min a b - c`.
|
Nat.add_mod_mod
theorem Nat.add_mod_mod : ∀ (m n k : ℕ), (m + n % k) % k = (m + n) % k
This theorem states that for all natural numbers `m`, `n`, and `k`, the remainder of the sum of `m` and the remainder of `n` divided by `k`, all divided by `k`, is equal to the remainder when `m + n` is divided by `k`. In mathematical terms, it's expressing the property `(m + n mod k) mod k = (m + n) mod k`.
More concisely: The theorem asserts that for all natural numbers `m`, `n`, and `k`, the remainder of `(m + n)` divided by `k` is equal to the remainder of `m` when divided by `k`, plus the remainder of `n` when divided by `k`. In Lean notation: `(m + n) mod k = (m mod k + n mod k) mod k`.
|
Nat.le_mul_of_pos_right
theorem Nat.le_mul_of_pos_right : ∀ {m : ℕ} (n : ℕ), 0 < m → n ≤ n * m
This theorem states that for all natural numbers 'm' and 'n', if 'm' is greater than 0, then 'n' is less than or equal to 'n' multiplied by 'm'. In other words, it's saying that any non-zero multiplication of a number will always be greater than or equal to the number itself.
More concisely: For all natural numbers m and n, if m > 0 then n <= n * m.
|
Nat.shiftLeft_succ
theorem Nat.shiftLeft_succ : ∀ (m n : ℕ), m <<< (n + 1) = 2 * m <<< n
This theorem, `Nat.shiftLeft_succ`, states that for any two natural numbers `m` and `n`, shifting `m` to the left by `n + 1` is equal to twice `m` shifted to the left by `n`. The left shift operation `<<<` can be thought of as multiplication by `2^n`, so this theorem essentially states that `m * 2^(n+1) = 2 * m * 2^n` for all natural numbers `m` and `n`.
More concisely: For all natural numbers `m` and `n`, `m <<< (n + 1) = 2 * (m <<< n)`.
|
Nat.max_eq_left
theorem Nat.max_eq_left : ∀ {a b : ℕ}, b ≤ a → max a b = a
This theorem states that for any two natural numbers `a` and `b`, if `b` is less than or equal to `a`, then the maximum of `a` and `b` is `a`. In other words, when comparing two natural numbers, if the second one is not larger than the first, the maximum of the two is the first number. This is a basic property of the maximum operation, which in this case is applied to natural numbers in Lean 4.
More concisely: For all natural numbers `a` and `b`, if `b` ≤ `a`, then max `a` `b` = `a`.
|
Nat.exists_eq_add_of_le
theorem Nat.exists_eq_add_of_le : ∀ {m n : ℕ}, m ≤ n → ∃ k, n = m + k
This theorem states that for any two natural numbers `m` and `n`, if `m` is less than or equal to `n`, then there exists a natural number `k` such that `n` is equal to the sum of `m` and `k`. In essence, it confirms that any natural number `n` greater than or equal to `m` can be expressed as the sum of `m` and some other natural number.
More concisely: For all natural numbers `m` and `n`, if `m ≤ n`, then there exists a natural number `k` such that `n = m + k`.
|