Nat.not_dvd_of_between_consec_multiples
theorem Nat.not_dvd_of_between_consec_multiples : ∀ {m n k : ℕ}, n * k < m → m < n * (k + 1) → ¬n ∣ m
This theorem states that for any natural numbers `m`, `n`, and `k`, if `m` is strictly greater than the product of `n` and `k` and strictly less than the product of `n` and `k + 1`, then `n` does not divide `m`. Essentially, the theorem is saying that if `m` is between two consecutive multiples of `n`, it cannot be divisible by `n`.
More concisely: If natural numbers `m`, `n`, and `k` satisfy `n * k < m < n * (k + 1)`, then `n` does not divide `m`.
|
Nat.le_div_iff_mul_le'
theorem Nat.le_div_iff_mul_le' : ∀ {a b c : ℕ}, 0 < b → (a ≤ c / b ↔ a * b ≤ c)
This theorem states that for all natural numbers `a`, `b`, and `c`, if `b` is greater than zero, then `a` is less than or equal to `c` divided by `b` if and only if `a` multiplied by `b` is less than or equal to `c`. In other words, the theorem provides a relationship between division and multiplication in the context of inequalities in natural numbers.
More concisely: For natural numbers `a`, `b`, and `c`, `a ≤ c / b` if and only if `a * b ≤ c`.
|
Nat.findGreatest_spec
theorem Nat.findGreatest_spec :
∀ {m : ℕ} {P : ℕ → Prop} [inst : DecidablePred P] {n : ℕ}, m ≤ n → P m → P (Nat.findGreatest P n)
The theorem `Nat.findGreatest_spec` states that for any natural number `m`, a predicate `P` which maps natural numbers to propositions, and a decidable instance `inst` for `P`, along with another natural number `n`, if `m` is less than or equal to `n` and `P m` holds true, then `P (Nat.findGreatest P n)` also holds true. In other words, if a certain property `P` holds for a number `m` up to `n`, then the same property holds for the greatest number where `P` is true up to `n`, as found by `Nat.findGreatest`.
More concisely: For any decidable predicate `P` on natural numbers, if `m` is less than or equal to `n` and `P(m)` holds, then `P(Nat.findGreatest P n)` also holds.
|
Mathlib.Data.Nat.Defs._auxLemma.6
theorem Mathlib.Data.Nat.Defs._auxLemma.6 : ∀ {m n : ℕ}, (m < n.succ) = (m ≤ n)
This theorem, from the Mathlib library in Lean 4, states that for any natural number `n`, adding 2 to `n` (i.e., `Nat.succ (Nat.succ n)`) results in a number that is greater than 1. In other words, for any natural number, its successor's successor is always greater than 1. The theorem is always true, regardless of the value of `n`.
More concisely: For any natural number `n`, `Nat.succ (Nat.succ n)` is greater than 1.
|
Nat.le_of_pred_lt
theorem Nat.le_of_pred_lt : ∀ {n : ℕ} {m : ℕ}, m.pred < n → m ≤ n
This theorem, `Nat.le_of_pred_lt`, states that for any two natural numbers `n` and `m`, if the predecessor of `m` (which is `m - 1` for non-zero `m` and `0` for `m = 0`) is less than `n`, then `m` is less than or equal to `n`. In other words, if `m - 1` is less than `n`, then it guarantees that `m` itself will not exceed `n`, which is a basic property of natural number ordering.
More concisely: If `m - 1` is less than `n`, then `m` is less than or equal to `n` for all natural numbers `m` and `n`.
|
Nat.sub_mod_eq_zero_of_mod_eq
theorem Nat.sub_mod_eq_zero_of_mod_eq : ∀ {m n k : ℕ}, m % k = n % k → (m - n) % k = 0
This theorem states that for any three natural numbers `m`, `n`, and `k`, if `m` modulo `k` equals to `n` modulo `k`, then the difference `m - n` modulo `k` equals zero. In mathematical notation, if m ≡ n (mod k), then (m - n) ≡ 0 (mod k). This theorem is useful in number theory, particularly in modular arithmetic, where the idea of congruence (expressed as 'equal mod `k`') is commonly used.
More concisely: If `m` is congruent to `n` modulo `k`, then `m - n` is congruent to zero modulo `k`.
|
Nat.find_le
theorem Nat.find_le : ∀ {n : ℕ} {p : ℕ → Prop} [inst : DecidablePred p] {h : ∃ n, p n}, p n → Nat.find h ≤ n
The theorem `Nat.find_le` states that for any natural number `n` and a predicate `p` that applies to natural numbers, given that `p` is a decidable predicate and there exists a natural number which satisfies the predicate `p`, if `n` satisfies `p`, then the least natural number that satisfies `p` (found by `Nat.find`) is less than or equal to `n`. This means that `Nat.find h` will always find the smallest natural number that satisfies the predicate `p`, or will be equal to `n` if `n` is the smallest such number.
More concisely: If `p` is a decidable predicate on natural numbers with an existentially quantified solution, and `n` is a natural number satisfying `p`, then the least natural number `m` such that `p(m)` holds (given by `Nat.find h`) is less than or equal to `n`.
|
Nat.mul_left_inj
theorem Nat.mul_left_inj : ∀ {a b c : ℕ}, a ≠ 0 → (b * a = c * a ↔ b = c)
This theorem, `Nat.mul_left_inj`, states that for any three natural numbers `a`, `b`, and `c`, if `a` is not equal to zero, then `b` times `a` equals `c` times `a` if and only if `b` equals `c`. In other words, the multiplication operation is left-injective in the natural numbers, assuming the left operand is not zero.
More concisely: For all natural numbers `a`, `b`, and `c`, if `a` is non-zero then `b * a = c * a` if and only if `b = c`.
|
Nat.add_succ_sub_one
theorem Nat.add_succ_sub_one : ∀ (m n : ℕ), m + n.succ - 1 = m + n
This theorem states that for all natural numbers `m` and `n`, the result of adding `n` incremented by one to `m` and then subtracting one is the same as just adding `n` to `m`. In mathematical notation, it asserts that for each pair of natural numbers `m` and `n`, the equation `m + (n + 1) - 1 = m + n` holds true.
More concisely: For all natural numbers `m` and `n`, `m + (n + 1) - 1` equals `m + n`.
|
Nat.one_lt_mul_iff
theorem Nat.one_lt_mul_iff : ∀ {m n : ℕ}, 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)
This theorem states that for any two natural numbers `m` and `n`, the product of `m` and `n` is greater than 1 if and only if both `m` and `n` are positive and at least one of them is greater than 1.
More concisely: For natural numbers `m` and `n`, `m * n > 1` if and only if both `m` and `n` are positive and at least one of them is greater than 1.
|
Nat.set_induction
theorem Nat.set_induction : ∀ {S : Set ℕ}, 0 ∈ S → (∀ k ∈ S, k + 1 ∈ S) → ∀ (n : ℕ), n ∈ S
This theorem states that for any subset of the set of natural numbers (`ℕ`), if the subset contains the number zero and any number `k` in the subset implies its successor `k + 1` is also in the subset, then the subset actually contains all natural numbers. In other words, this theorem establishes a form of mathematical induction over subsets of natural numbers, based on the principles that the subset contains zero and is closed under the successor function.
More concisely: If a subset of natural numbers (`ℕ`) contains zero and is closed under the successor function, then it contains all natural numbers.
|
Nat.two_le_iff
theorem Nat.two_le_iff : ∀ (n : ℕ), 2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1
This theorem states that for any natural number 'n', 'n' is greater than or equal to 2 if and only if 'n' is not equal to 0 and 'n' is not equal to 1. In other words, any natural number 'n' being greater than or equal to 2 is equivalent to 'n' being different from both 0 and 1.
More concisely: For any natural number n, n ≥ 2 if and only if n ≠ 0 ∧ n ≠ 1.
|
Nat.dvd_div_iff
theorem Nat.dvd_div_iff : ∀ {a b c : ℕ}, c ∣ b → (a ∣ b / c ↔ c * a ∣ b)
This theorem states that for all natural numbers `a`, `b`, and `c`, if `c` is a divisor of `b`, then `a` divides `b / c` if and only if `c * a` divides `b`. In other words, it establishes a connection between the divisibility of `b` by `a` and `c * a` under the assumption that `c` is a divisor of `b`.
More concisely: For all natural numbers `a`, `b`, and `c`, if `c` divides `b`, then `a` divides `b / c` if and only if `c * a` divides `b`.
|
Nat.dvd_right_iff_eq
theorem Nat.dvd_right_iff_eq : ∀ {m n : ℕ}, (∀ (a : ℕ), m ∣ a ↔ n ∣ a) ↔ m = n
This theorem states that two natural numbers, `m` and `n`, are equal if and only if they have the same set of multiples. In other words, if every natural number `a` is a multiple of `m` if and only if it is a multiple of `n`, then `m` and `n` must be the same number.
More concisely: Two natural numbers `m` and `n` are equal if and only if they have the same set of multiples.
|
LT.lt.nat_succ_le
theorem LT.lt.nat_succ_le : ∀ {n m : ℕ}, n < m → n.succ ≤ m
This theorem, `LT.lt.nat_succ_le`, is an alias for `Nat.succ_le_of_lt`. It states that for any two natural numbers `n` and `m`, if `n` is less than `m`, then the successor of `n` (which is `n` plus 1, denoted as `Nat.succ n` in Lean 4) is less than or equal to `m`.
More concisely: If `n` is less than `m` in the natural numbers, then `Nat.succ n` is less than or equal to `m`.
|
Nat.mul_self_le_mul_self_iff
theorem Nat.mul_self_le_mul_self_iff : ∀ {m n : ℕ}, m * m ≤ n * n ↔ m ≤ n
This theorem states that for all natural numbers `m` and `n`, the condition of `m` squared (or `m` multiplied by itself) being less than or equal to `n` squared (or `n` multiplied by itself) is equivalent to `m` being less than or equal to `n`. This theorem essentially establishes a relation to compare the square of two natural numbers and the numbers themselves.
More concisely: For all natural numbers m and n, m ^ 2 ≤ n ^ 2 if and only if m ≤ n.
|
Nat.le_succ_iff
theorem Nat.le_succ_iff : ∀ {m n : ℕ}, m ≤ n.succ ↔ m ≤ n ∨ m = n.succ
This theorem, `Nat.le_succ_iff`, states that for all natural numbers `m` and `n`, the condition `m` is less than or equal to `n + 1` is equivalent to either `m` is less than or equal to `n` or `m` is equal to `n + 1`. In other words, a natural number `m` being less than or equal to the successor of another natural number `n`, can happen either if `m` is less than or equal to `n`, or if `m` is exactly the successor of `n`.
More concisely: For all natural numbers m and n, m is less than or equal to n + 1 if and only if m is less than or equal to n or m is equal to n + 1.
|
Nat.leRecOn_self
theorem Nat.leRecOn_self :
∀ {C : ℕ → Sort u_1} {n : ℕ} {next : {k : ℕ} → C k → C (k + 1)} (x : C n), Nat.leRecOn ⋯ (fun {k} => next) x = x
This theorem states that for any natural number `n` and a function `next` that takes a natural number `k` and a value of some type `C k` and produces a value of type `C (k + 1)`, when `Nat.leRecOn` is applied to `n`, the function `next`, and a value `x` of type `C n`, the result is `x`. In other words, the least number recursion on `n` using `next` and starting with `x` just gives `x` again.
More concisely: For any function `next : ℕ → C → C` and value `x : C n`, `Nat.leRecOn n next x = x`.
|
Nat.mul_self_lt_mul_self
theorem Nat.mul_self_lt_mul_self : ∀ {m n : ℕ}, m < n → m * m < n * n
This theorem states that for any two natural numbers 'm' and 'n', if 'm' is less than 'n', then the square of 'm' is also less than the square of 'n'. Specifically, the theorem is applicable to all pairs of natural numbers where the first is strictly less than the second.
More concisely: For all natural numbers m and n, if m < n then m^2 < n^2.
|
Nat.succ_inj
theorem Nat.succ_inj : ∀ {a b : ℕ}, a.succ = b.succ ↔ a = b
This is a theorem about the successor function (which adds one) on natural numbers in Lean 4. It states that for any two natural numbers `a` and `b`, the successor of `a` is equal to the successor of `b` if and only if `a` is equal to `b`. Essentially, this means that adding one to two different natural numbers will yield two different results unless the original natural numbers were the same. This theorem is also known as an alias of `Nat.succ_inj'`.
More concisely: The successor function is injective on natural numbers, i.e., for all natural numbers `a` and `b`, if `Nat.succ a = Nat.succ b` then `a = b`.
|
Nat.sub_succ'
theorem Nat.sub_succ' : ∀ (m n : ℕ), m - n.succ = m - n - 1
This theorem, called `Nat.sub_succ'`, states that for every two natural numbers `m` and `n`, subtracting the successor of `n` from `m` is equal to first subtracting `n` from `m` and then subtracting 1. In other words, `m - (n + 1)` is equal to `(m - n) - 1`. This theorem is an alternate version of `Nat.sub_succ` but in a more intuitive format using subtraction by 1 instead of the predecessor function.
More concisely: For all natural numbers `m` and `n`, `m - (n + 1)` equals `(m - n) - 1`.
|
Nat.pred_one_add
theorem Nat.pred_one_add : ∀ (n : ℕ), (1 + n).pred = n
This theorem states that for every natural number `n`, the predecessor of `(1 + n)` is `n`. Here, `pred` refers to the predecessor function in natural numbers, which returns the previous natural number. In other words, if you add 1 to any natural number `n` and then find the predecessor of the result, you will get the original number `n` back.
More concisely: For all natural numbers n, pred(1 + n) = n.
|
Nat.pow_right_injective
theorem Nat.pow_right_injective : ∀ {a : ℕ}, 2 ≤ a → Function.Injective fun x => a ^ x
The theorem `Nat.pow_right_injective` states that for every natural number `a` that is greater than or equal to 2, the function that raises `a` to the power of another natural number `x` is injective. In other words, if `a` is a natural number greater than or equal to 2, then for any two natural numbers `x` and `y`, if `a^x = a^y`, then `x` must equal to `y`.
More concisely: For every natural number `a` greater than or equal to 2, the function `x => a^x` is injective (i.e., if `a^x = a^y`, then `x = y`).
|
Nat.lt_of_lt_pred
theorem Nat.lt_of_lt_pred : ∀ {m n : ℕ}, m < n - 1 → m < n
This theorem states that for any two natural numbers `m` and `n`, if `m` is less than `n - 1`, then `m` is also less than `n`. In other words, if a number `m` is less than another number `n` minus one, then `m` is also less than `n`. This is intuitively true because reducing `n` by one results in a number smaller than `n`, so if `m` is smaller than that, it must also be smaller than `n`.
More concisely: If `m` is a natural number and `m` < `n` implies `m` < `(n - 1)`, then `m` < `n` holds in the natural numbers.
|
Nat.leRecOn_succ
theorem Nat.leRecOn_succ :
∀ {C : ℕ → Sort u_1} {n m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
Nat.leRecOn h2 next x = next (Nat.leRecOn h1 (fun {k} => next) x)
The theorem `Nat.leRecOn_succ` is a property of recursively defined functions on natural numbers in Lean 4. Specifically, it defines how a function, denoted here as `next`, behaves when applied to a specific case of the recursive structure `Nat.leRecOn`. The theorem states that for any natural numbers `n` and `m` such that `n ≤ m`, a function `C` from natural numbers to a type, a function `next` modifying `C`, and an element `x : C n`, the result of applying `Nat.leRecOn` to `n ≤ m + 1` and `next` and `x`, is the same as applying `next` to the result of `Nat.leRecOn` applied to `n ≤ m` and the same `next` and `x`. This theorem ensures a consistent behavior of recursive functions across different values of natural numbers.
More concisely: For any recursively defined function `next` on natural numbers, `Nat.leRecOn (n ≤ m + 1) (next) (x)` equals `next (Nat.leRecOn (n ≤ m) (next) (x))`, where `n ≤ m` holds and `x : C n`.
|
Nat.lt_add_one_iff
theorem Nat.lt_add_one_iff : ∀ {m n : ℕ}, m < n + 1 ↔ m ≤ n
This theorem, `Nat.lt_add_one_iff`, states that for any two natural numbers `m` and `n`, `m` is less than `n` plus one if and only if `m` is less than or equal to `n`. It essentially provides a relationship between the "less than" and "less than or equal to" operations in the context of natural numbers, particularly when dealing with the incrementation of a number.
More concisely: For natural numbers `m` and `n`, `m` is less than `n` + 1 if and only if `m` is less than or equal to `n`.
|
Nat.lt_pred_iff
theorem Nat.lt_pred_iff : ∀ {a b : ℕ}, a < b.pred ↔ a.succ < b
This theorem, `Nat.lt_pred_iff`, establishes a relationship between the 'less than' operation on natural numbers and the predecessor function. It states that for any two natural numbers `a` and `b`, `a` is less than the predecessor of `b` if and only if the successor of `a` is less than `b`. The predecessor function returns the preceding natural number or zero if the input is zero, while the successor function returns the succeeding natural number.
More concisely: For all natural numbers a and b, a < Suc(b) if and only if Suc(a) < b, where Suc denotes the successor function.
|
Nat.one_le_of_lt
theorem Nat.one_le_of_lt : ∀ {a b : ℕ}, a < b → 1 ≤ b
This theorem states that for any two natural numbers `a` and `b`, if `a` is less than `b`, then `b` is greater than or equal to 1. In other words, if a natural number is greater than another natural number, then it is always at least 1.
More concisely: For all natural numbers `a` and `b`, if `a < b`, then `b >= 1`.
|
Nat.one_le_pow
theorem Nat.one_le_pow : ∀ (n m : ℕ), 0 < m → 1 ≤ m ^ n
This theorem states that for every pair of natural numbers `n` and `m`, if `m` is greater than zero, then 1 is less than or equal to `m` raised to the power of `n`. In other words, any positive natural number raised to any natural number power is always at least 1.
More concisely: For all natural numbers n and m with m > 0, m^n ≥ 1.
|
Nat.pow_lt_pow_left
theorem Nat.pow_lt_pow_left : ∀ {a b : ℕ}, a < b → ∀ {n : ℕ}, n ≠ 0 → a ^ n < b ^ n
This theorem states that for any two natural numbers 'a' and 'b', if 'a' is less than 'b', then 'a' raised to any non-zero natural number 'n' will be less than 'b' raised to the 'n'. In other words, for all natural numbers 'a', 'b', and 'n', where 'a' is less than 'b' and 'n' is not zero, $a^n$ is less than $b^n$.
More concisely: For all natural numbers $a, b, n$ with $a < b$ and $n \neq 0$, $a^n < b^n$.
|
Nat.add_one_le_iff
theorem Nat.add_one_le_iff : ∀ {m n : ℕ}, m + 1 ≤ n ↔ m < n
This theorem, `Nat.add_one_le_iff`, states a property about natural numbers. For every pair of natural numbers `m` and `n`, the statement that `m + 1` is less than or equal to `n` is equivalent to the statement that `m` is strictly less than `n`.
More concisely: For all natural numbers m and n, m + 1 < n if and only if m < n.
|
Nat.findGreatest_le
theorem Nat.findGreatest_le : ∀ {P : ℕ → Prop} [inst : DecidablePred P] (n : ℕ), Nat.findGreatest P n ≤ n
The theorem `Nat.findGreatest_le` states that for any natural number `n` and any decidable predicate `P` on natural numbers, the greatest natural number `i` less than or equal to `n` for which `P(i)` holds is always less than or equal to `n`. If there is no such `i` (i.e., if `P(i)` does not hold for any `i` less than or equal to `n`), then by definition, `Nat.findGreatest P n` is `0`, which is also less than or equal to `n`. This theorem is a property of the `Nat.findGreatest` function in Lean 4, which finds the greatest natural number that satisfies a given predicate.
More concisely: For any natural number `n` and decidable predicate `P` on natural numbers, the greatest `i` (if it exists) less than or equal to `n` with `P(i)` holding is less than or equal to `n`, and if no such `i` exists, then `Nat.findGreatest P n = 0`.
|
Mathlib.Data.Nat.Defs._auxLemma.31
theorem Mathlib.Data.Nat.Defs._auxLemma.31 : ∀ {a b : ℕ}, (a.succ = b.succ) = (a = b)
This theorem, `Mathlib.Data.Nat.Defs._auxLemma.31`, states that for any natural number `i`, `i` is less than or equal to `0` if and only if `i` equals `0`. In other words, the only natural number less than or equal to `0` is `0` itself.
More concisely: For any natural number `i`, `i` is less than or equal to `0` if and only if `i` equals `0`.
|
Nat.pow_two_sub_pow_two
theorem Nat.pow_two_sub_pow_two : ∀ (a b : ℕ), a ^ 2 - b ^ 2 = (a + b) * (a - b)
The theorem `Nat.pow_two_sub_pow_two` is an alias of `Nat.sq_sub_sq` in Lean 4. It states that for any two natural numbers `a` and `b`, the difference of their squares, i.e., `a` squared minus `b` squared, is equal to the product of the sum `(a + b)` and the difference `(a - b)` of these two natural numbers. This is a standard formula in algebra often called the difference of squares formula.
More concisely: For all natural numbers `a` and `b`, `(a ^ 2) - (b ^ 2)` equals `(a + b) * (a - b)`.
|
Nat.le_mul_self
theorem Nat.le_mul_self : ∀ (n : ℕ), n ≤ n * n
This theorem, known as `Nat.le_mul_self`, states that for all natural numbers `n`, `n` is less than or equal to the square of `n`. That is, for every natural number `n`, the inequality `n ≤ n * n` holds true. This is a basic property of multiplication in the natural numbers.
More concisely: For all natural numbers `n`, `n` is less than or equal to `n * n`.
|
Nat.not_dvd_iff_between_consec_multiples
theorem Nat.not_dvd_iff_between_consec_multiples :
∀ (n : ℕ) {a : ℕ}, 0 < a → ((∃ k, a * k < n ∧ n < a * (k + 1)) ↔ ¬a ∣ n)
This theorem states that for any natural number `n` and any non-zero natural number `a`, `n` is not divisible by `a` if and only if `n` is located between `a * k` and `a * (k + 1)` for some natural number `k`. Essentially, if `n` is not a multiple of `a`, it must fall in between two consecutive multiples of `a`.
More concisely: For any natural numbers `n` and `a` with `a` being non-zero, `n` is not divisible by `a` if and only if there exists a natural number `k`, such that `a * k < n < a * (k + 1)`.
|
Nat.dvd_left_iff_eq
theorem Nat.dvd_left_iff_eq : ∀ {m n : ℕ}, (∀ (a : ℕ), a ∣ m ↔ a ∣ n) ↔ m = n
This theorem states that for any two natural numbers `m` and `n`, they are equal if and only if they have the same divisors. In other words, if every number `a` that divides `m` also divides `n` and vice versa, then `m` and `n` are indeed the same number.
More concisely: Two natural numbers `m` and `n` are equal if and only if they have the same divisors.
|
Nat.div_mod_unique
theorem Nat.div_mod_unique : ∀ {a b c d : ℕ}, 0 < b → (a / b = d ∧ a % b = c ↔ c + b * d = a ∧ c < b)
This theorem states that for any four natural numbers `a`, `b`, `c`, and `d` where `b` is greater than zero, the division of `a` by `b` resulting in `d` and the remainder as `c` is logically equivalent to the condition where the sum of `c` and the product of `b` and `d` equals `a` and `c` is less than `b`. This forms a fundamental property of division and modulo operations in number theory.
More concisely: For natural numbers `a`, `b` (with `b > 0`), `c`, and `d`, the conditions `a = b * d + c` and `0 <= c < b` are logically equivalent.
|
Nat.sqrt_le
theorem Nat.sqrt_le : ∀ (n : ℕ), n.sqrt * n.sqrt ≤ n
This theorem states that for any natural number `n`, the square of its integer square root (calculated using the `Nat.sqrt` function) is less than or equal to `n` itself. In other words, for all `n` in the set of natural numbers, the inequality $(\text{Nat.sqrt } n)^2 \leq n$ holds. This is a property of integer square roots, reflecting the fact that they are the largest whole number whose square does not exceed the original number.
More concisely: For all natural numbers `n`, the square of their integer square root (obtained from `Nat.sqrt`) is less than or equal to `n`. In mathematical notation: `(sqrt n)^2 ≤ n`.
|
Nat.leRecOn_trans
theorem Nat.leRecOn_trans :
∀ {C : ℕ → Sort u_1} {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
Nat.leRecOn ⋯ next x = Nat.leRecOn hmk next (Nat.leRecOn hnm next x)
This theorem states that for any natural numbers `n`, `m`, and `k` where `n` is less than or equal to `m` and `m` is less than or equal to `k`, and any function `next` that takes a natural number `k` and a value of type `C k` and produces a value of type `C (k + 1)`, and any value `x` of type `C n`, the result of applying the function `Nat.leRecOn` (which recursively applies `next` starting with `x` until it reaches a certain natural number) to `n`, `m`, and `k` with `next` and `x` is equivalent to applying `Nat.leRecOn` to `m` and `k` with `next` and the result of applying `Nat.leRecOn` to `n` and `m` with `next` and `x`.
More concisely: For any natural numbers `n ≤ m ≤ k` and function `next : ℕ → C → C`, if `Nat.leRecOn n m k next x = y` then `Nat.leRecOn m k next y = Nat.leRecOn n m next x`.
|
Nat.not_dvd_of_pos_of_lt
theorem Nat.not_dvd_of_pos_of_lt : ∀ {m n : ℕ}, 0 < n → n < m → ¬m ∣ n
This theorem states that for any two natural numbers `m` and `n`, if `n` is positive and less than `m`, then `m` does not divide `n`. In mathematical terms, this theorem states that if 0 < n < m for n, m ∈ ℕ, then m does not divide n.
More concisely: For all natural numbers m and n, if 0 < n < m then m does not divide n.
|
Nat.mod_add_div'
theorem Nat.mod_add_div' : ∀ (a b : ℕ), a % b + a / b * b = a
This theorem states that for any two natural numbers `a` and `b`, the sum of the remainder of `a` divided by `b` (`a % b`) and the product of the quotient of `a` divided by `b` (`a / b`) and `b` is equal to `a`. In mathematical terms, this can be written as `a mod b + ⌊a / b⌋ * b = a`. It essentially describes a property of the division algorithm in the natural numbers.
More concisely: For any natural numbers `a` and `b`, the theorem asserts that `a = (a % b) + ⌊a / b⌋ * b`.
|
Nat.sqrt_lt
theorem Nat.sqrt_lt : ∀ {m n : ℕ}, m.sqrt < n ↔ m < n * n
This theorem is about the relationship between the integer square root function and multiplication in the set of natural numbers. It states that for any two natural numbers `m` and `n`, the square root of `m` is less than `n` if and only if `m` is less than the square of `n`. In mathematical terms, it can be expressed as $\sqrt{m} < n \iff m < n^2$ for all natural numbers `m` and `n`.
More concisely: The natural square root of a natural number is less than another natural number if and only if the first number is less than the square of the second number. In Lean 4, this is expressed as $\sqrt{m} < n \iff m < n^2$ for all natural numbers $m$ and $n$.
|
Nat.div_eq_zero_iff
theorem Nat.div_eq_zero_iff : ∀ {a b : ℕ}, 0 < b → (a / b = 0 ↔ a < b)
This theorem states that for any two natural numbers `a` and `b`, if `b` is greater than 0, then the quotient of `a` divided by `b` equals 0 if and only if `a` is less than `b`. That is, in the context of natural numbers, a number `a` divided by another number `b` (where `b` is non-zero) yields a result of zero precisely when `a` is smaller than `b`.
More concisely: For natural numbers `a` and `b` with `b > 0`, `a / b = 0` if and only if `a < b`.
|
Nat.mul_right_inj
theorem Nat.mul_right_inj : ∀ {a b c : ℕ}, a ≠ 0 → (a * b = a * c ↔ b = c)
This theorem states that for any natural numbers `a`, `b`, and `c`, if `a` is not zero, then `a` multiplied by `b` equals `a` multiplied by `c` if and only if `b` equals `c`. In other words, multiplication by a non-zero natural number on the right is injective, i.e., it preserves distinctness. This means if two natural numbers are distinct, then their products with a non-zero natural number will also be distinct.
More concisely: For any natural numbers `a` (not equal to zero) and `b` and `c`, `a * b = a * c` if and only if `b = c`.
|
Nat.succ_le_iff
theorem Nat.succ_le_iff : ∀ {m n : ℕ}, m.succ ≤ n ↔ m < n
This theorem states a relationship between two natural number operations in mathematics. Specifically, for any two natural numbers `m` and `n`, the successor of `m` (which is `m` + 1) is less than or equal to `n` if and only if `m` is less than `n`.
More concisely: For all natural numbers m and n, m < n if and only if m + 1 <= n.
|
Nat.mul_self_le_mul_self
theorem Nat.mul_self_le_mul_self : ∀ {m n : ℕ}, m ≤ n → m * m ≤ n * n
This theorem states that for any two natural numbers `m` and `n`, if `m` is less than or equal to `n`, then `m` squared (i.e., `m` multiplied by itself) is also less than or equal to `n` squared (i.e., `n` multiplied by itself). In mathematical notation, this states that ∀ m, n ∈ ℕ (m ≤ n → m² ≤ n²).
More concisely: For all natural numbers m and n, if m <= n then m^2 <= n^2.
|
Nat.mul_dvd_of_dvd_div
theorem Nat.mul_dvd_of_dvd_div : ∀ {a b c : ℕ}, c ∣ b → a ∣ b / c → c * a ∣ b
This theorem states that for any three natural numbers `a`, `b`, and `c`, if `c` divides `b` and `a` divides the result of `b` divided by `c`, then `c` times `a` must divide `b`. This theorem is a property of divisibility and division in the domain of natural numbers.
More concisely: If `c` divides `b` and `a` divides `b` divided by `c`, then `c` times `a` divides `b`.
|
Nat.find_mono
theorem Nat.find_mono :
∀ {p q : ℕ → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q],
(∀ (n : ℕ), q n → p n) → ∀ {hp : ∃ n, p n} {hq : ∃ n, q n}, Nat.find hp ≤ Nat.find hq
The `Nat.find_mono` theorem states that for any two decidable predicates `p` and `q` on natural numbers, if for every natural number `n`, `q(n)` implies `p(n)`, then for any `n` that satisfies `p` (`hp`) and any `n` that satisfies `q` (`hq`), the least natural number that satisfies `p` is less than or equal to the least natural number that satisfies `q`. In other words, if `q` implies `p`, then the smallest number that satisfies `q` cannot be less than the smallest number that satisfies `p`.
More concisely: If `p` implies `q` and both `p` and `q` are decidable predicates on natural numbers, then the least natural number satisfying `p` is less than or equal to the least natural number satisfying `q`.
|
Nat.one_lt_pow
theorem Nat.one_lt_pow : ∀ {a n : ℕ}, n ≠ 0 → 1 < a → 1 < a ^ n
This theorem states that for any natural numbers `a` and `n`, if `n` is not equal to 0 and `a` is greater than 1, then the value of `a` raised to the power of `n` (denoted as `a ^ n`) will be greater than 1. In other words, any natural number greater than 1, when raised to any non-zero natural number, will yield a result greater than 1.
More concisely: For all natural numbers `a` greater than 1 and `n` non-zero, `a^n > 1`.
|
Nat.dvd_left_injective
theorem Nat.dvd_left_injective : Function.Injective fun x x_1 => x ∣ x_1
The theorem `Nat.dvd_left_injective` states that the "divides" function (`dvd`), when viewed as a function of its left argument, is injective. This means that if `x` and `y` are any two natural numbers and if `x` divides some number `n` exactly the same way as `y` does, then `x` and `y` must actually be the same number.
More concisely: If `x` and `y` are natural numbers such that `n` is dividable by both `x` and `y` in the same way, then `x` and `y` are equal.
|
Nat.of_le_succ
theorem Nat.of_le_succ : ∀ {m n : ℕ}, m ≤ n.succ → m ≤ n ∨ m = n.succ
This theorem, `Nat.of_le_succ`, provides an alias for the forward direction of the `Nat.le_succ_iff` theorem. Specifically, it states that for any two natural numbers `m` and `n`, if `m` is less than or equal to the successor of `n` (or `n` incremented by 1), then either `m` is less than or equal to `n` or `m` is equal to the successor of `n`.
More concisely: If `m` is less than or equal to `n` + 1, then `m` is less than or equal to `n` or `m` equals `n` + 1.
|
Nat.sqrt_eq
theorem Nat.sqrt_eq : ∀ (n : ℕ), (n * n).sqrt = n
The theorem `Nat.sqrt_eq` states that for every natural number `n`, the integer square root of the square of `n` is equal to `n` itself. In other words, if we square a natural number and then take its integer square root, we will arrive back at the original number. This corresponds to the mathematical statement: $\forall n \in \mathbb{N}, \ \sqrt{n^2} = n$.
More concisely: For every natural number $n$, the integer square root of $n^2$ equals $n$. In other words, $\sqrt{n^2} = n$.
|
Nat.le_findGreatest
theorem Nat.le_findGreatest :
∀ {m : ℕ} {P : ℕ → Prop} [inst : DecidablePred P] {n : ℕ}, m ≤ n → P m → m ≤ Nat.findGreatest P n
This theorem, `Nat.le_findGreatest`, asserts that for any natural number `m` and a decidable predicate `P` (a predicate for which we can definitively say whether it is true or false), if `m` is less than or equal to `n` and `P(m)` holds true, then `m` is less than or equal to the greatest natural number `i` less than or equal to `n` for which `P(i)` holds. In other words, if `m` satisfies the predicate `P` and is within the bounds of `n`, it cannot be larger than the greatest such number that fulfills these conditions.
More concisely: For all natural numbers `m` and `n` and decidable predicate `P`, if `m` is less than or equal to `n` and `P(m)` holds, then `m` is less than or equal to the greatest `i` less than or equal to `n` with `P(i)` holding.
|
Nat.lt_succ_sqrt
theorem Nat.lt_succ_sqrt : ∀ (n : ℕ), n < n.sqrt.succ * n.sqrt.succ
This theorem states that for any natural number `n`, `n` is strictly less than the square of the successor of the integer square root of `n`. In mathematical terms, for any natural number `n`, we have `n < (sqrt(n) + 1)^2`. This is using the integer square root function `Nat.sqrt`, which is implemented using Newton's method and takes a natural number as input. The successor function `Nat.succ` increments a natural number by one.
More concisely: For every natural number `n`, `n` is strictly less than the square of the successor of the integer square root of `n`. In mathematical notation, `n < (1 + sqrt n)²`.
|
Nat.set_induction_bounded
theorem Nat.set_induction_bounded : ∀ {n k : ℕ} {S : Set ℕ}, k ∈ S → (∀ k ∈ S, k + 1 ∈ S) → k ≤ n → n ∈ S
This theorem states that for any subset `S` of natural numbers `ℕ`, any arbitrary natural numbers `n` and `k`, if `k` is an element of `S` and `S` is closed under successor operation (meaning if `k` is in `S`, then `k + 1` is also in `S`), then every natural number `n` that is greater than or equal to `k` is also an element of `S`.
More concisely: If `S` is a subset of natural numbers that contains `k` and is closed under the successor operation, then every natural number greater than or equal to `k` is in `S`.
|
Nat.findGreatest_eq_zero_iff
theorem Nat.findGreatest_eq_zero_iff :
∀ {k : ℕ} {P : ℕ → Prop} [inst : DecidablePred P], Nat.findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n := by
sorry
The theorem `Nat.findGreatest_eq_zero_iff` states that for any natural number `k` and any predicate `P` on natural numbers, where `P` is a decidable predicate, the greatest natural number less than or equal to `k` for which `P` holds is `0` if and only if for every natural number `n` greater than `0` and less than or equal to `k`, the predicate `P` does not hold for `n`. In other words, `P` does not hold for any natural numbers in the range from `1` to `k`.
More concisely: For any decidable predicate P on natural numbers, the greatest natural number less than or equal to k with property P is 0 if and only if no natural number n, with 0 < n <= k, has property P.
|
Nat.lt_pow_self
theorem Nat.lt_pow_self : ∀ {a : ℕ}, 1 < a → ∀ (n : ℕ), n < a ^ n
This theorem states that for any natural number 'a' greater than 1, and for any natural number 'n', 'n' is less than 'a' to the power of 'n'. In other words, the value of 'n' is always less than the value of 'a' raised to the 'n'-th power, given 'a' is greater than one.
More concisely: For any natural number $a > 1$, and any natural number $n$, $n < a^n$.
|
Nat.dvd_add_right
theorem Nat.dvd_add_right : ∀ {a b c : ℕ}, a ∣ b → (a ∣ b + c ↔ a ∣ c)
This theorem states that for any three natural numbers `a`, `b`, and `c`, if `a` divides `b`, then `a` divides `b + c` if and only if `a` divides `c`. This sets a necessary and sufficient condition for `a` to divide the sum of `b` and `c` based on the divisibility of `a` and `c`. In mathematical terms, we write this as "a | b implies (a | (b + c) iff a | c)".
More concisely: A natural number `a` divides the sum `b + c` of natural numbers `b` and `c` if and only if `a` divides `c` (i.e., `a | b -> a | (b + c) <-> a | c`).
|
Nat.le_induction
theorem Nat.le_induction :
∀ {m : ℕ} {P : (n : ℕ) → m ≤ n → Prop},
P m ⋯ → (∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯) → ∀ (n : ℕ) (hmn : m ≤ n), P n hmn
This is the induction principle starting at a non-zero number. For any natural number `m` and a property `P` that depends on a natural number `n` and the fact that `m` is less than or equal to `n`, if `P` holds for `m` and if, for any `n` where `P` holds, then `P` also holds for `n + 1`, then `P` holds for any `n` that is greater than or equal to `m`. This theorem is typically used in an induction proof with the syntax `induction n, hn using Nat.le_induction`.
More concisely: The theorem states that if a property `P` holds for a natural number `m` less than or equal to `n`, and `P` holds for `n + 1` whenever it holds for `n`, then `P` holds for all natural numbers greater than or equal to `m`. (Natural number induction principle)
|
Nat.find_eq_iff
theorem Nat.find_eq_iff :
∀ {m : ℕ} {p : ℕ → Prop} [inst : DecidablePred p] (h : ∃ n, p n), Nat.find h = m ↔ p m ∧ ∀ n < m, ¬p n
The theorem `Nat.find_eq_iff` in Lean 4 expresses a property of the `Nat.find` function in terms of logical equivalence. It states that for any natural number `m` and any decidable predicate `p` on natural numbers, and given that there exists a natural number `n` such that `p(n)` holds, then `Nat.find h` is equal to `m` if and only if `p(m)` is true and for all natural numbers `n` less than `m`, `p(n)` is not true. In essence, this theorem characterizes the least natural number satisfying a given decidable predicate.
More concisely: For any natural number `m` and decidable predicate `p` on natural numbers, `Nat.find h = m` if and only if `p(m)` holds and `p(n)` fails for all `n` strictly less than `m`.
|
Nat.eq_zero_of_dvd_of_lt
theorem Nat.eq_zero_of_dvd_of_lt : ∀ {a b : ℕ}, a ∣ b → b < a → b = 0
This theorem asserts that if a small natural number 'b' is divisible by a larger natural number 'a', then the small number 'b' must be zero. In other words, no small natural number can be evenly divisible by a larger one, unless the small number is zero. This is a fundamental principle of number division in natural numbers.
More concisely: A smaller natural number cannot be evenly divided by a larger natural number, except for the case where the smaller number is zero.
|
Nat.one_le_iff_ne_zero
theorem Nat.one_le_iff_ne_zero : ∀ {n : ℕ}, 1 ≤ n ↔ n ≠ 0
This theorem states that for any natural number `n`, the condition "1 is less than or equal to `n`" is logically equivalent to the condition "`n` is not equal to 0". In other words, in the domain of natural numbers, `n` being non-zero is the same as `n` being at least 1.
More concisely: The theorem asserts that for all natural numbers `n`, the condition `1 ≤ n` is logically equivalent to `n ≠ 0`.
|
Nat.div_pos
theorem Nat.div_pos : ∀ {a b : ℕ}, b ≤ a → 0 < b → 0 < a / b
This theorem states that for any two natural numbers `a` and `b`, if `b` is less than or equal to `a` and `b` is greater than 0, then the result of dividing `a` by `b` is also greater than 0. Essentially, it asserts that the division of a larger natural number by a smaller, positive natural number is always a positive natural number.
More concisely: For all natural numbers `a` and `b` with `0 < b <= a`, the quotient `a / b` is a positive natural number.
|
Nat.sqrt_add_eq
theorem Nat.sqrt_add_eq : ∀ {a : ℕ} (n : ℕ), a ≤ n + n → (n * n + a).sqrt = n
This theorem states that for any natural number `n` and for any other natural number `a` such that `a` is less than or equal to twice `n`, the square root (calculated using the `Nat.sqrt` function) of the sum of the square of `n` and `a` is equal to `n`. In mathematical notation, this is stating that for all $n, a \in \mathbb{N}$ such that $a \leq 2n$, we have $\sqrt{n^2 + a} = n$.
More concisely: For any natural numbers $n$ and $a$ with $a \leq 2n$, we have $\sqrt{n^2 + a} = n$.
|
Nat.findGreatest_mono
theorem Nat.findGreatest_mono :
∀ {m : ℕ} {P Q : ℕ → Prop} [inst : DecidablePred P] {n : ℕ} [inst_1 : DecidablePred Q],
(∀ (n : ℕ), P n → Q n) → m ≤ n → Nat.findGreatest P m ≤ Nat.findGreatest Q n
The theorem `Nat.findGreatest_mono` states that, given two natural number predicates `P` and `Q` and natural numbers `m` and `n`, if every natural number `n` that satisfies `P` also satisfies `Q`, and `m` is less than or equal to `n`, then the largest `i ≤ m` for which `P i` holds is less than or equal to the largest `i ≤ n` for which `Q i` holds. This is, if we have two properties of natural numbers such that property `Q` is stronger or equivalent to property `P` (every number that has property `P` also has property `Q`) and we are comparing numbers up to `m` for `P` and `n` for `Q` where `m ≤ n`, then the largest number that has property `P` is less than or equal to the largest number that has property `Q`. This theorem requires decidability of the predicates `P` and `Q`.
More concisely: If `P` is a decidable natural number predicate that is monotonically included in another decidable natural number predicate `Q`, then the maximum natural number `i ≤ m` such that `P i` holds is less than or equal to the maximum natural number `i ≤ n` such that `Q i` holds.
|
Nat.mul_dvd_mul_iff_left
theorem Nat.mul_dvd_mul_iff_left : ∀ {a b c : ℕ}, 0 < a → (a * b ∣ a * c ↔ b ∣ c)
This theorem states that for any three natural numbers `a`, `b`, and `c`, given that `a` is greater than `0`, the product of `a` and `b` divides the product of `a` and `c` if and only if `b` divides `c`. In other words, it says that if `a` is a non-zero factor common to both sides of the divisibility relation, then it can be "cancelled out".
More concisely: For natural numbers a, b, and c with a > 0, a * b | (a * c) if and only if b | c. (a * b is the product of a and b, | denotes divisibility, and b | c means b divides c.)
|
Nat.div_le_div_right
theorem Nat.div_le_div_right : ∀ {a b c : ℕ}, a ≤ b → a / c ≤ b / c
This theorem states that for all natural numbers `a`, `b`, and `c`, if `a` is less than or equal to `b`, then the result of integer division of `a` by `c` is less than or equal to the result of integer division of `b` by `c`. In other words, increasing the numerator in a division operation doesn't decrease the division's result.
More concisely: For all natural numbers a, b, and c, if a ≤ b then a / c ≤ b / c.
|
Nat.succ_succ_ne_one
theorem Nat.succ_succ_ne_one : ∀ (n : ℕ), n.succ.succ ≠ 1
This theorem states that for all natural numbers `n`, the successor of the successor of `n` is not equal to one. In other words, if you start with any natural number and increment it twice, you will never end up with the number one. This makes intuitive sense because the minimum natural number is zero and incrementing it twice gives two, which is not equal to one.
More concisely: For all natural numbers `n`, `(S (S n)) ≠ 1`, where `S` denotes the successor function.
|
Nat.le_sqrt
theorem Nat.le_sqrt : ∀ {m n : ℕ}, m ≤ n.sqrt ↔ m * m ≤ n
This theorem, `Nat.le_sqrt`, in Lean 4 states a property about the square root of natural numbers. For any two natural numbers `m` and `n`, `m` is less than or equal to the square root of `n` if and only if the square of `m` is less than or equal to `n`. This theorem provides a connection between the integer square root function and the standard inequality of natural numbers.
More concisely: For all natural numbers m and n, m ≤ √n if and only if m² ≤ n.
|
Nat.div_lt_self'
theorem Nat.div_lt_self' : ∀ (a b : ℕ), (a + 1) / (b + 2) < a + 1
This theorem states that for any two natural numbers `a` and `b`, the integer division of (`a + 1`) by (`b + 2`) is strictly less than (`a + 1`). This is a version of the `Nat.div_lt_self` theorem, but it uses successors (i.e., adding 1 to a number) instead of additional hypotheses.
More concisely: For all natural numbers `a` and `b`, `(a + 1) / (b + 2)` is strictly less than `a + 1`.
|
Mathlib.Data.Nat.Defs._auxLemma.1
theorem Mathlib.Data.Nat.Defs._auxLemma.1 : ∀ (n : ℕ), (n < 0) = False
This theorem, `Mathlib.Data.Nat.Defs._auxLemma.1`, states that for any natural number `n`, the condition that `n` is less than zero is always `False`. In other words, it's asserting that no natural number can be less than zero. This aligns with the definition of natural numbers in mathematics, which includes all whole numbers from zero upwards.
More concisely: For any natural number `n`, `n` is not less than zero.
|
Nat.mod_succ
theorem Nat.mod_succ : ∀ (n : ℕ), n % n.succ = n
This theorem states that for any natural number `n`, the remainder of `n` divided by its successor (`n+1`) is `n` itself. It essentially demonstrates a property of the modulus operation in the context of natural numbers, where the divisor is the successor of the dividend. This is a reflection of the fact that `n+1` is greater than `n`, so when `n` is divided by `n+1`, the remainder is `n`.
More concisely: For all natural numbers `n`, `n` is the remainder when `n` is divided by `n+1`.
|
Nat.not_exists_sq
theorem Nat.not_exists_sq : ∀ {m n : ℕ}, m * m < n → n < (m + 1) * (m + 1) → ¬∃ t, t * t = n
The theorem states that for all natural numbers `m` and `n`, if `n` is strictly greater than the square of `m` but is also strictly less than the square of `m+1`, then there does not exist any natural number `t` such that `t` squared equals `n`. In other words, there are no perfect squares strictly between `m²` and `(m+1)²`.
More concisely: For all natural numbers `m` and `n`, if `m² < n < (m+1)²`, then `n` is not the square of any natural number.
|
Nat.diag_induction
theorem Nat.diag_induction :
∀ (P : ℕ → ℕ → Prop),
(∀ (a : ℕ), P (a + 1) (a + 1)) →
(∀ (b : ℕ), P 0 (b + 1)) →
(∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)) → ∀ (a b : ℕ), a < b → P a b
The theorem `Nat.diag_induction` states that given a predicate `P` with two natural number inputs, if `P (a + 1) (a + 1)` holds true for all natural numbers `a`, `P 0 (b + 1)` holds true for all natural numbers `b`, and whenever `a` is less than `b`, both `P (a + 1) b` and `P a (b + 1)` being true implies that `P (a + 1) (b + 1)` is also true, then `P a b` is true for all natural numbers `a` less than `b`. This theorem outlines a kind of diagonal induction on pairs of natural numbers.
More concisely: Given a predicate `P` satisfying `P (a + 1) (a + 1)` for all `a`, `P 0 (b + 1)` for all `b`, and `P (a + 1) b` and `P a (b + 1)` imply `P (a + 1) (b + 1)` for all `a < b`, then `P a b` holds for all `a < b`.
|
Nat.lt_one_iff
theorem Nat.lt_one_iff : ∀ {n : ℕ}, n < 1 ↔ n = 0
This theorem states that for any natural number `n`, `n` is less than 1 if and only if `n` is equal to 0. In more formal mathematical terms, for all natural numbers `n`, the proposition `n < 1` is logically equivalent to the proposition `n = 0`.
More concisely: For any natural number `n`, `n` is less than 1 if and only if `n` equals 0. (Equivalently, `n < 1` if and only if `n = 0`.)
|
Nat.div_dvd_of_dvd
theorem Nat.div_dvd_of_dvd : ∀ {m n : ℕ}, n ∣ m → m / n ∣ m
This theorem establishes a property of division in the context of natural numbers. Specifically, it asserts that for any two natural numbers 'm' and 'n', if 'n' divides 'm' (denoted by `n ∣ m`), then the result of integer division of 'm' by 'n' (denoted by `m / n`) also divides 'm'. This theorem can be useful when dealing with problems related to divisibility and factorization in number theory.
More concisely: If a natural number 'n' divides another natural number 'm', then 'm' divided by 'n' is a natural number that also divides 'm'.
|
Nat.succ_injective
theorem Nat.succ_injective : Function.Injective Nat.succ
The theorem `Nat.succ_injective` states that the successor function `Nat.succ` on natural numbers is injective. In other words, for any two natural numbers `a` and `b`, if the successor of `a` (denoted as `Nat.succ a`) is equal to the successor of `b` (denoted as `Nat.succ b`), then `a` must be equal to `b`. This is a property of the "next number" or "successor" function in the set of natural numbers.
More concisely: If for natural numbers `a` and `b`, `Nat.succ a = Nat.succ b`, then `a = b`.
|
Nat.one_lt_iff_ne_zero_and_ne_one
theorem Nat.one_lt_iff_ne_zero_and_ne_one : ∀ {n : ℕ}, 1 < n ↔ n ≠ 0 ∧ n ≠ 1
This theorem is stating that for any natural number `n`, the condition `1 < n` is equivalent to the conditions `n ≠ 0` and `n ≠ 1`. In other words, a natural number `n` is greater than one if and only if `n` is not equal to zero and `n` is not equal to one.
More concisely: For any natural number `n`, the conditions `1 < n`, `n ≠ 0`, and `n ≠ 1` are equivalent.
|
Nat.one_lt_succ_succ
theorem Nat.one_lt_succ_succ : ∀ (n : ℕ), 1 < n.succ.succ
This theorem states that for any natural number `n`, the number 1 is less than the successor (or the next number) of the successor of `n`. In mathematical terms, this theorem asserts that 1 < n + 2 for all natural numbers `n`.
More concisely: For all natural numbers `n`, the number 1 is less than the successor of `n`, or equivalently, `1 < n + 2`.
|
Nat.div_lt_iff_lt_mul'
theorem Nat.div_lt_iff_lt_mul' : ∀ {a b c : ℕ}, 0 < b → (a / b < c ↔ a < c * b)
This theorem, `Nat.div_lt_iff_lt_mul'`, states that for all natural numbers `a`, `b`, and `c`, if `b` is greater than zero, then `a` divided by `b` is less than `c` if and only if `a` is less than `c` multiplied by `b`. In other words, it establishes a relationship between division and multiplication in terms of inequality for natural numbers.
More concisely: For all natural numbers `a`, `b`, and `c` with `b > 0`, `a / b < c` if and only if `a < c * b`.
|
Nat.lt_iff_add_one_le
theorem Nat.lt_iff_add_one_le : ∀ {m n : ℕ}, m < n ↔ m + 1 ≤ n
This theorem, named `Nat.lt_iff_add_one_le`, establishes an equivalence relation for natural numbers `m` and `n`. It states that `m` is less than `n` if and only if `m + 1` is less than or equal to `n`. In other words, the number `m` is considered to be smaller than the number `n` precisely when the successor of `m` (i.e., `m` incremented by 1) is not larger than `n`.
More concisely: For all natural numbers m and n, m < n if and only if m + 1 <= n.
|
Nat.one_mod
theorem Nat.one_mod : ∀ (n : ℕ), 1 % (n + 2) = 1
This theorem declares that for all natural numbers `n`, the remainder of 1 divided by `n + 2` is always 1. In other words, when 1 is divided by any natural number greater than or equal to 2 (which is `n+2`), the remainder is invariably 1.
More concisely: For all natural numbers n, 1 has a remainder of 1 when divided by n + 2.
|
Nat.mul_div_cancel_left'
theorem Nat.mul_div_cancel_left' : ∀ {a b : ℕ}, a ∣ b → a * (b / a) = b
This theorem states that for any two natural numbers `a` and `b`, if `a` divides `b`, then `a` multiplied by the result of `b` divided by `a` equals `b`. In mathematical terms, if `a` is a divisor of `b`, then `a*(b/a) = b`. This reflects the property of division and multiplication being inverse operations under certain conditions in the set of natural numbers.
More concisely: If `a` divides `b` in the natural numbers, then `a * (b / a) = b`.
|
Nat.dvd_add_self_left
theorem Nat.dvd_add_self_left : ∀ {m n : ℕ}, m ∣ m + n ↔ m ∣ n
This theorem states that for any natural numbers `m` and `n`, `m` divides the sum of `m` and `n` if and only if `m` divides `n`. In other words, if `m` is a factor of the sum `m + n`, it must also be a factor of `n`, and vice versa; if `m` is a factor of `n`, it is also a factor of the sum `m + n`.
More concisely: For natural numbers m and n, m divides both n and m + n if and only if it divides n.
|
Nat.dvd_add_self_right
theorem Nat.dvd_add_self_right : ∀ {m n : ℕ}, m ∣ n + m ↔ m ∣ n
This theorem in Lean 4 states that for any natural numbers 'm' and 'n', 'm' divides the sum 'n + m' if and only if 'm' divides 'n'. In other words, if a natural number 'm' can be a divisor of its own sum with another natural number 'n', then it necessarily implies that 'm' is also a divisor of 'n', and vice versa.
More concisely: For natural numbers m and n, m divides n if and only if m divides (n + m).
|
Nat.findGreatest_eq_iff
theorem Nat.findGreatest_eq_iff :
∀ {m k : ℕ} {P : ℕ → Prop} [inst : DecidablePred P],
Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
The theorem `Nat.findGreatest_eq_iff` states that for any natural numbers `m` and `k`, and any predicate `P` in natural numbers that is decidable, `Nat.findGreatest P k` is equal to `m` if and only if the following conditions are met: `m` is less than or equal to `k`, if `m` is not zero then `P m` holds, and for every natural number `n` greater than `m` but less than or equal to `k`, `P n` does not hold. In other words, `m` is the greatest natural number less than or equal to `k` for which the predicate `P` holds.
More concisely: For any decidable predicate P on natural numbers and natural numbers m and k with m <= k and P(m) holding if m is non-zero, m is the greatest natural number less than or equal to k satisfying P if and only if no natural number n between m and k satisfies P.
|
Nat.leRecOn_succ'
theorem Nat.leRecOn_succ' :
∀ {C : ℕ → Sort u_1} {n : ℕ} {h : n ≤ n + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
Nat.leRecOn h (fun {k} => next) x = next x
This theorem, `Nat.leRecOn_succ'`, asserts that for any natural number `n` and any function `next` that takes a natural number `k` and a value of some type `C k` (dependent on `k`) to provide a value of type `C (k + 1)`, if we apply `Nat.leRecOn` for the proof that `n` is less than or equal to `n + 1` using `next` as the function and `x` as the initial value, we get the same output as if we had directly applied `next` to `x`. In other words, it states that the recursive operation on natural numbers respects the successor operation in the provided function `next`.
More concisely: For any natural number `n` and function `next : Nat → C → C`, if `Nat.leRecOn n next x` is defined, then `next x = next (S n)`.
|