Nat.descFactorial_eq_div
theorem Nat.descFactorial_eq_div : ∀ {n k : ℕ}, k ≤ n → n.descFactorial k = n.factorial / (n - k).factorial
This theorem establishes an equivalent expression for the descending factorial of a natural number `n` taken `k` at a time, where `k` is less than or equal to `n`. Specifically, it states that the descending factorial of `n` and `k` is equal to the factorial of `n` divided by the factorial of `(n - k)`. However, it is recommended to avoid using this theorem in favor of `Nat.factorial_mul_descFactorial` if possible, because working with natural number division can be problematic.
More concisely: The descending factorial of a natural number `n` taken `k` at a time is equal to the quotient of the factorial of `n` by the factorial of `(n - k)`, where `0 ≤ k ≤ n`.
|
Nat.factorial_mul_descFactorial
theorem Nat.factorial_mul_descFactorial : ∀ {n k : ℕ}, k ≤ n → (n - k).factorial * n.descFactorial k = n.factorial := by
sorry
This theorem states that for any two natural numbers 'n' and 'k', where 'k' is less than or equal to 'n', the product of the factorial of 'n - k' and the factorial of 'n' descending by 'k' steps, is equal to the factorial of 'n'. It is a version of the formula `n.descFactorial k = n! / (n - k)!` that avoids using division over natural numbers.
More concisely: For any natural numbers n and k with k <= n, the product of the factorial of (n-k) and the descending factorial of n by k is equal to the factorial of n.
|
Nat.factorial_pos
theorem Nat.factorial_pos : ∀ (n : ℕ), 0 < n.factorial
The theorem `Nat.factorial_pos` states that for every natural number `n`, the factorial of `n`, denoted by `Nat.factorial n`, is always greater than 0. In other words, the factorial function always returns a positive natural number when applied to any natural number.
More concisely: For every natural number `n`, `Nat.factorial n` is a positive natural number.
|
Nat.self_le_factorial
theorem Nat.self_le_factorial : ∀ (n : ℕ), n ≤ n.factorial
The theorem `Nat.self_le_factorial` states that for all natural numbers `n`, `n` is less than or equal to the factorial of `n`. In other words, any natural number is always less than or equal to its factorial.
More concisely: For all natural numbers `n`, `n` is less than or equal to the factorial of `n` (`n ≤ factorial n`).
|
Nat.descFactorial_zero
theorem Nat.descFactorial_zero : ∀ (n : ℕ), n.descFactorial 0 = 1
The theorem `Nat.descFactorial_zero` asserts that for any natural number `n`, the descending factorial `Nat.descFactorial n 0` is equal to `1`. This is equivalent to the mathematical statement that $n^{\underline{0}}=1$, where $n^{\underline{0}}$ denotes the descending factorial. This is consistent with the general pattern in factorials that anything to the power of zero is one.
More concisely: For any natural number $n$, the descending factorial $n^{\underline{0}}$ equals 1.
|
Nat.factorial_mul_ascFactorial
theorem Nat.factorial_mul_ascFactorial : ∀ (n k : ℕ), n.factorial * (n + 1).ascFactorial k = (n + k).factorial := by
sorry
The theorem `Nat.factorial_mul_ascFactorial` states that for any two natural numbers `n` and `k`, the factorial of `n` times the ascending factorial of `n + 1` to `k` is equal to the factorial of `n + k`. Here, the ascending factorial is the product of consecutive natural numbers starting from `n + 1` and ending at `n + k - 1`. Note that this statement does not involve the concept of division in the natural numbers. A corresponding theorem `Nat.ascFactorial_eq_div` contains a similar equation using natural number division.
More concisely: For any natural numbers `n` and `k`, `(n! * (n + 1)! * ... * (n + k - 1)!) = (n + k)!`.
|
Nat.factorial_le
theorem Nat.factorial_le : ∀ {m n : ℕ}, m ≤ n → m.factorial ≤ n.factorial
The theorem `Nat.factorial_le` states that for any two natural numbers `m` and `n`, if `m` is less than or equal to `n`, then the factorial of `m` is also less than or equal to the factorial of `n`. In other words, the factorial function on natural numbers is monotone non-decreasing. This is expressed using the notation of order in natural numbers: `m ≤ n` implies `Nat.factorial m ≤ Nat.factorial n`.
More concisely: For all natural numbers m and n, if m <= n then Nat.factorial m <= Nat.factorial n.
|
Nat.factorial_one
theorem Nat.factorial_one : Nat.factorial 1 = 1
This theorem, `Nat.factorial_one`, asserts that the factorial of 1 is 1. In mathematical terms, it simply states that `1! = 1`, where "!" is the factorial operation, which multiplies a given natural number by all natural numbers less than it down to one. In this specific case, since there are no natural numbers less than one, the factorial of one is simply one itself.
More concisely: The theorem asserts that 1! = 1.
|
Nat.ascFactorial_succ
theorem Nat.ascFactorial_succ : ∀ {n k : ℕ}, n.ascFactorial k.succ = (n + k) * n.ascFactorial k
The theorem `Nat.ascFactorial_succ` states that for any two natural numbers `n` and `k`, the ascending factorial of `n` and `k + 1` (represented in Lean as `Nat.ascFactorial n (Nat.succ k)`) is equal to the product of `(n + k)` and the ascending factorial of `n` and `k` (represented as `(n + k) * Nat.ascFactorial n k`). In mathematical terms, the ascending factorial `n.ascFactorial (k + 1)` is equal to the product `(n + k) * n.ascFactorial k`. This essentially captures the recursive nature of the ascending factorial operation.
More concisely: For all natural numbers n and k, Nat.ascFactorial (Nat.succ n) (Nat.succ k) = (n + k) * Nat.ascFactorial n k.
|
Nat.factorial_zero
theorem Nat.factorial_zero : Nat.factorial 0 = 1
The theorem `Nat.factorial_zero` states that the factorial of 0 is 1. In mathematical terms, this is denoted as `0! = 1`. This is a fundamental property in combinatorics, as there is exactly one way to arrange zero items.
More concisely: The theorem `Nat.factorial_zero` asserts that the factorial of 0 equals 1 (i.e., 0! = 1).
|
Nat.factorial_dvd_factorial
theorem Nat.factorial_dvd_factorial : ∀ {m n : ℕ}, m ≤ n → m.factorial ∣ n.factorial
The theorem `Nat.factorial_dvd_factorial` states that for any two natural numbers `m` and `n`, if `m` is less than or equal to `n`, then the factorial of `m` (denoted by `Nat.factorial m`) divides the factorial of `n` (denoted by `Nat.factorial n`). In other words, `Nat.factorial n` is a multiple of `Nat.factorial m` whenever `m ≤ n`. This is a well-known property of factorials in mathematics.
More concisely: For all natural numbers m and n with m ≤ n, Nat.factorial m | Nat.factorial n. (Here, | denotes divisibility.)
|
Nat.factorial_mul_ascFactorial'
theorem Nat.factorial_mul_ascFactorial' :
∀ (n k : ℕ), 0 < n → (n - 1).factorial * n.ascFactorial k = (n + k - 1).factorial
This theorem states that for any two natural numbers `n` and `k`, where `n` is greater than 0, the product of the factorial of `(n - 1)` and the ascending factorial of `n` taken `k` times is equal to the factorial of `(n + k - 1)`. It provides a way to compute the ascending factorial without needing to perform natural number division, hence avoiding the complications of natural number subtraction. The theorem `Nat.ascFactorial_eq_div` provides an equivalent formulation that does involve natural number division. You might also consider using the `factorial_mul_ascFactorial` theorem to further avoid these complications.
More concisely: For any natural numbers `n` and `k` with `n > 0`, the product of `(n - 1)!` and `k` ascending factorials of `n` is equal to `(n + k - 1)!`.
|
Nat.ascFactorial_eq_div
theorem Nat.ascFactorial_eq_div : ∀ (n k : ℕ), (n + 1).ascFactorial k = (n + k).factorial / n.factorial
This theorem states that for any two natural numbers `n` and `k`, the ascending factorial of `n + 1` and `k` is equal to the division of the factorial of `n + k` by the factorial of `n`. However, it is recommended to avoid this theorem in favor of `Nat.factorial_mul_ascFactorial` if possible due to the complications associated with natural number division.
More concisely: For any natural numbers `n` and `k`, the ascending factorial `(n + 1)!` equals the quotient of `n + k` factorial `!(n + k)` by `n!`.
|
Nat.ascFactorial_eq_div'
theorem Nat.ascFactorial_eq_div' : ∀ (n k : ℕ), 0 < n → n.ascFactorial k = (n + k - 1).factorial / (n - 1).factorial
This theorem states that for any two natural numbers `n` and `k` where `n` is greater than zero, the ascending factorial of `n` and `k` is equal to the factorial of `(n + k - 1)` divided by the factorial of `(n - 1)`. However, this theorem should be avoided in favor of `Nat.factorial_mul_ascFactorial'` if possible, since division in ℕ (natural numbers) is not recommended.
More concisely: For any natural number `n` greater than zero, the ascending factorial `n `** `k` equals `(factorial (n + k - 1)) / (factorial (n - 1))`.
|
Nat.factorial_ne_zero
theorem Nat.factorial_ne_zero : ∀ (n : ℕ), n.factorial ≠ 0
The theorem `Nat.factorial_ne_zero` states that for every natural number `n`, the factorial of `n` is not equal to zero. In mathematical terminology, this can be written as: for all natural numbers `n`, `n! ≠ 0`. This corresponds to the well-known fact that the factorial of any natural number is always positive, since it is a product of positive integers.
More concisely: For every natural number `n`, the factorial `n!` is non-zero.
|
Nat.factorial_lt
theorem Nat.factorial_lt : ∀ {m n : ℕ}, 0 < n → (n.factorial < m.factorial ↔ n < m)
This theorem, named `Nat.factorial_lt`, states that for any two natural numbers `m` and `n`, given that `n` is greater than zero, the factorial of `n` is less than the factorial of `m` if and only if `n` is less than `m`. In other words, it establishes a direct correspondence between the order of two natural numbers and the order of their factorials, under the condition that the second number is positive.
More concisely: For natural numbers m and n with n > 0, m > n if and only if m! < n!.
|
Nat.factorial_succ
theorem Nat.factorial_succ : ∀ (n : ℕ), (n + 1).factorial = (n + 1) * n.factorial
The theorem `Nat.factorial_succ` states that for all natural numbers `n`, the factorial of `n + 1` is equal to `(n + 1) times the factorial of `n`. This corresponds to the recursive definition of the factorial function in mathematics, where the factorial of a number `n` (denoted as `n!`) is `n` multiplied by the factorial of `n - 1`.
More concisely: The theorem `Nat.factorial_succ` asserts that for all natural numbers `n`, `(n + 1)! = (n + 1) * n!`.
|
Nat.factorial_mul_pow_le_factorial
theorem Nat.factorial_mul_pow_le_factorial : ∀ {m n : ℕ}, m.factorial * (m + 1) ^ n ≤ (m + n).factorial
This theorem, `Nat.factorial_mul_pow_le_factorial`, asserts that for all natural numbers `m` and `n`, the factorial of `m` times `(m + 1)` raised to the power of `n` is less than or equal to the factorial of `(m + n)`. In other words, it states that for any two natural numbers, the factorial of the first number times the increment of the first number raised to the power of the second number will never exceed the factorial of the sum of these two numbers.
More concisely: For all natural numbers m and n, m!*(m + 1)^n ≤ (m + n)!.
|
Nat.succ_ascFactorial
theorem Nat.succ_ascFactorial : ∀ (n k : ℕ), n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
This theorem states that for any natural numbers `n` and `k`, the product of `n` and the ascending factorial of `n+1` and `k` equals the product of `n+k` and the ascending factorial of `n` and `k`. Here, the ascending factorial `Nat.ascFactorial n k` is defined as the product `n * (n + 1) * ... * (n + k - 1)`.
More concisely: For all natural numbers `n` and `k`, the product of `n` with the ascending factorial of `n+1` and `k` equals the product of `n+k` with the ascending factorial of `n` and `k`. In other words, `n * Nat.ascFactorial (n+1) k = (n+k) * Nat.ascFactorial n k`.
|
Nat.ascFactorial_zero
theorem Nat.ascFactorial_zero : ∀ (n : ℕ), n.ascFactorial 0 = 1
This theorem states that for any natural number `n`, the ascending factorial of `n` with 0 as the second argument is equal to 1. In other words, it states that the product of an empty sequence of consecutive natural numbers, starting from any given natural number `n`, is always 1.
More concisely: For any natural number `n`, the product of the empty sequence of natural numbers starting from `n` is equal to 1.
|
Nat.descFactorial_of_lt
theorem Nat.descFactorial_of_lt : ∀ {n k : ℕ}, n < k → n.descFactorial k = 0
This theorem, `Nat.descFactorial_of_lt`, states that for any two natural numbers 'n' and 'k', if 'n' is less than 'k', then the descending factorial of 'n' and 'k' is zero. The descending factorial, denoted as `n.descFactorial k`, is a variation of the factorial operation where the product decreases at each step, instead of remaining constant as in the standard factorial.
More concisely: For all natural numbers n and k, if n < k then n.descFactorial k = 0.
|
Nat.descFactorial_succ
theorem Nat.descFactorial_succ : ∀ (n k : ℕ), n.descFactorial (k + 1) = (n - k) * n.descFactorial k
The theorem `Nat.descFactorial_succ` states that for any two natural numbers `n` and `k`, the descending factorial of `n` at `(k + 1)` is equal to the product of `(n - k)` and the descending factorial of `n` at `k`. In mathematical terms, this means that `n.descFactorial (k + 1) = (n - k) * n.descFactorial k`. The descending factorial, `n.descFactorial k`, is defined as the factorial of `n` divided by the factorial of `(n - k)`, implemented recursively.
More concisely: The descending factorial of a natural number `n` at `k+1` equals the product of `(n-k)` and the descending factorial of `n` at `k`. In other words, `n.descFactorial (k+1) = (n-k) * n.descFactorial k`.
|