# Factorial and variants #

This file defines the factorial, along with the ascending and descending variants. For the proof that the factorial of `n` counts the permutations of an `n`-element set, see `Fintype.card_perm`.

## Main declarations #

- `Nat.factorial`: The factorial.
- `Nat.ascFactorial`: The ascending factorial. It is the product of natural numbers from `n` to `n + k - 1`.
- `Nat.descFactorial`: The descending factorial. It is the product of natural numbers from `n - k + 1` to `n`.

source
def Nat.factorial :
ℕ → ℕ

`Nat.factorial n` is the factorial of `n`.

Equations

- Nat.factorial 0 = 1
- n.succ.factorial = n.succ * n.factorial

Instances For

source
def Nat.term_! :
Lean.TrailingParserDescr

factorial notation `(n)!` for `Nat.factorial n`. In Lean, names can end with exclamation marks (e.g. `List.get!`), so you cannot write `n!` in Lean, but must write `(n)!` or `n !` instead. The former is preferred, since Lean can confuse the `!` in `n !` as the (prefix) Boolean negation operation in some cases. For numerals the parentheses are not required, so e.g. `0!` or `1!` work fine. Todo: replace occurrences of `n !` with `(n)!` in Mathlib.

Equations

- Nat.term_! = Lean.ParserDescr.trailingNode `Nat.term_! 10000 0 (Lean.ParserDescr.symbol "!")

Instances For

source
@[simp]
theorem Nat.factorial_zero :
factorial 0 = 1
source
theorem Nat.factorial_succ (n : ℕ) :
(n + 1).factorial = (n + 1) * n.factorial
source
@[simp]
theorem Nat.factorial_one :
factorial 1 = 1
source
@[simp]
theorem Nat.factorial_two :
factorial 2 = 2
source
theorem Nat.mul_factorial_pred {n : ℕ} (hn : n ≠ 0) :
n * (n - 1).factorial = n.factorial
source
theorem Nat.factorial_pos (n : ℕ) :
0 < n.factorial
source
theorem Nat.factorial_ne_zero (n : ℕ) :
n.factorial ≠ 0
source
theorem Nat.factorial_dvd_factorial {m n : ℕ} (h : m ≤ n) :
m.factorial ∣ n.factorial
source
theorem Nat.dvd_factorial {m n : ℕ} :
0 < m → m ≤ n → m ∣ n.factorial
source
theorem Nat.factorial_le {m n : ℕ} (h : m ≤ n) :
m.factorial ≤ n.factorial
source
theorem Nat.factorial_mul_pow_le_factorial {m n : ℕ} :
m.factorial * (m + 1) ^ n ≤ (m + n).factorial
source
theorem Nat.factorial_lt {m n : ℕ} (hn : 0 < n) :
n.factorial < m.factorial ↔ n < m
source
theorem Nat.factorial_lt_of_lt {m n : ℕ} (hn : 0 < n) (h : n < m) :
n.factorial < m.factorial
source
@[simp]
theorem Nat.one_lt_factorial {n : ℕ} :
1 < n.factorial ↔ 1 < n
source
@[simp]
theorem Nat.factorial_eq_one {n : ℕ} :
n.factorial = 1 ↔ n ≤ 1
source
theorem Nat.factorial_inj {m n : ℕ} (hn : 1 < n) :
n.factorial = m.factorial ↔ n = m
source
theorem Nat.factorial_inj' {m n : ℕ} (h : 1 < n ∨ 1 < m) :
n.factorial = m.factorial ↔ n = m
source
theorem Nat.self_le_factorial (n : ℕ) :
n ≤ n.factorial
source
theorem Nat.lt_factorial_self {n : ℕ} (hi : 3 ≤ n) :
n < n.factorial
source
theorem Nat.add_factorial_succ_lt_factorial_add_succ {i : ℕ} (n : ℕ) (hi : 2 ≤ i) :
i + (n + 1).factorial < (i + n + 1).factorial
source
theorem Nat.add_factorial_lt_factorial_add {i n : ℕ} (hi : 2 ≤ i) (hn : 1 ≤ n) :
i + n.factorial < (i + n).factorial
source
theorem Nat.add_factorial_succ_le_factorial_add_succ (i n : ℕ) :
i + (n + 1).factorial ≤ (i + (n + 1)).factorial
source
theorem Nat.add_factorial_le_factorial_add (i : ℕ) {n : ℕ} (n1 : 1 ≤ n) :
i + n.factorial ≤ (i + n).factorial
source
theorem Nat.factorial_mul_pow_sub_le_factorial {n m : ℕ} (hnm : n ≤ m) :
n.factorial * n ^ (m - n) ≤ m.factorial
source
theorem Nat.factorial_le_pow (n : ℕ) :
n.factorial ≤ n ^ n

### Ascending and descending factorials #

source
def Nat.ascFactorial (n : ℕ) :
ℕ → ℕ

`n.ascFactorial k = n (n + 1) ⋯ (n + k - 1)`. This is closely related to `ascPochhammer`, but much less general.

Equations

- n.ascFactorial 0 = 1
- n.ascFactorial n_1.succ = (n + n_1) * n.ascFactorial n_1

Instances For

source
@[simp]
theorem Nat.ascFactorial_zero (n : ℕ) :
n.ascFactorial 0 = 1
source
theorem Nat.ascFactorial_succ {n k : ℕ} :
n.ascFactorial k.succ = (n + k) * n.ascFactorial k
source
theorem Nat.zero_ascFactorial (k : ℕ) :
ascFactorial 0 k.succ = 0
source
@[simp]
theorem Nat.one_ascFactorial (k : ℕ) :
ascFactorial 1 k = k.factorial
source
theorem Nat.succ_ascFactorial (n k : ℕ) :
n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
source
theorem Nat.factorial_mul_ascFactorial (n k : ℕ) :
n.factorial * (n + 1).ascFactorial k = (n + k).factorial

`(n + 1).ascFactorial k = (n + k) ! / n !` but without ℕ-division. See `Nat.ascFactorial_eq_div` for the version with ℕ-division.

source
theorem Nat.factorial_mul_ascFactorial' (n k : ℕ) (h : 0 < n) :
(n - 1).factorial * n.ascFactorial k = (n + k - 1).factorial

`n.ascFactorial k = (n + k - 1)! / (n - 1)!` for `n > 0` but without ℕ-division. See `Nat.ascFactorial_eq_div` for the version with ℕ-division. Consider using `factorial_mul_ascFactorial` to avoid complications of ℕ-subtraction.

source
theorem Nat.ascFactorial_mul_ascFactorial (n l k : ℕ) :
n.ascFactorial l * (n + l).ascFactorial k = n.ascFactorial (l + k)
source
theorem Nat.ascFactorial_eq_div (n k : ℕ) :
(n + 1).ascFactorial k = (n + k).factorial / n.factorial

Avoid in favor of `Nat.factorial_mul_ascFactorial` if you can. ℕ-division isn't worth it.

source
theorem Nat.ascFactorial_eq_div' (n k : ℕ) (h : 0 < n) :
n.ascFactorial k = (n + k - 1).factorial / (n - 1).factorial

Avoid in favor of `Nat.factorial_mul_ascFactorial'` if you can. ℕ-division isn't worth it.

source
theorem Nat.ascFactorial_of_sub {n k : ℕ} :
(n - k) * (n - k + 1).ascFactorial k = (n - k).ascFactorial (k + 1)
source
theorem Nat.pow_succ_le_ascFactorial (n k : ℕ) :
n ^ k ≤ n.ascFactorial k
source
theorem Nat.pow_lt_ascFactorial' (n k : ℕ) :
(n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)
source
theorem Nat.pow_lt_ascFactorial (n : ℕ) {k : ℕ} :
2 ≤ k → (n + 1) ^ k < (n + 1).ascFactorial k
source
theorem Nat.ascFactorial_le_pow_add (n k : ℕ) :
(n + 1).ascFactorial k ≤ (n + k) ^ k
source
theorem Nat.ascFactorial_lt_pow_add (n : ℕ) {k : ℕ} :
2 ≤ k → (n + 1).ascFactorial k < (n + k) ^ k
source
theorem Nat.ascFactorial_pos (n k : ℕ) :
0 < (n + 1).ascFactorial k
source
def Nat.descFactorial (n : ℕ) :
ℕ → ℕ

`n.descFactorial k = n! / (n - k)!` (as seen in `Nat.descFactorial_eq_div`), but implemented recursively to allow for "quick" computation when using `norm_num`. This is closely related to `descPochhammer`, but much less general.

Equations

- n.descFactorial 0 = 1
- n.descFactorial n_1.succ = (n - n_1) * n.descFactorial n_1

Instances For

source
@[simp]
theorem Nat.descFactorial_zero (n : ℕ) :
n.descFactorial 0 = 1
source
@[simp]
theorem Nat.descFactorial_succ (n k : ℕ) :
n.descFactorial (k + 1) = (n - k) * n.descFactorial k
source
theorem Nat.zero_descFactorial_succ (k : ℕ) :
descFactorial 0 (k + 1) = 0
source
theorem Nat.descFactorial_one (n : ℕ) :
n.descFactorial 1 = n
source
theorem Nat.succ_descFactorial_succ (n k : ℕ) :
(n + 1).descFactorial (k + 1) = (n + 1) * n.descFactorial k
source
theorem Nat.succ_descFactorial (n k : ℕ) :
(n + 1 - k) * (n + 1).descFactorial k = (n + 1) * n.descFactorial k
source
theorem Nat.descFactorial_self (n : ℕ) :
n.descFactorial n = n.factorial
source
@[simp]
theorem Nat.descFactorial_eq_zero_iff_lt {n k : ℕ} :
n.descFactorial k = 0 ↔ n < k
source
@[simp]
theorem Nat.descFactorial_pos {n k : ℕ} :
0 < n.descFactorial k ↔ k ≤ n
source
theorem Nat.descFactorial_of_lt {n k : ℕ} :
n < k → n.descFactorial k = 0

Alias of the reverse direction of `Nat.descFactorial_eq_zero_iff_lt`.

source
theorem Nat.add_descFactorial_eq_ascFactorial (n k : ℕ) :
(n + k).descFactorial k = (n + 1).ascFactorial k
source
theorem Nat.add_descFactorial_eq_ascFactorial' (n k : ℕ) :
(n + k - 1).descFactorial k = n.ascFactorial k
source
theorem Nat.factorial_mul_descFactorial {n k : ℕ} :
k ≤ n → (n - k).factorial * n.descFactorial k = n.factorial

`n.descFactorial k = n! / (n - k)!` but without ℕ-division. See `Nat.descFactorial_eq_div` for the version using ℕ-division.

source
theorem Nat.descFactorial_mul_descFactorial {k m n : ℕ} (hkm : k ≤ m) :
(n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m
source
theorem Nat.descFactorial_eq_div {n k : ℕ} (h : k ≤ n) :
n.descFactorial k = n.factorial / (n - k).factorial

Avoid in favor of `Nat.factorial_mul_descFactorial` if you can. ℕ-division isn't worth it.

source
theorem Nat.descFactorial_le (n : ℕ) {k m : ℕ} (h : k ≤ m) :
k.descFactorial n ≤ m.descFactorial n
source
theorem Nat.pow_sub_le_descFactorial (n k : ℕ) :
(n + 1 - k) ^ k ≤ n.descFactorial k
source
theorem Nat.pow_sub_lt_descFactorial' {n k : ℕ} :
k + 2 ≤ n → (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
source
theorem Nat.pow_sub_lt_descFactorial {n k : ℕ} :
2 ≤ k → k ≤ n → (n + 1 - k) ^ k < n.descFactorial k
source
theorem Nat.descFactorial_le_pow (n k : ℕ) :
n.descFactorial k ≤ n ^ k
source
theorem Nat.descFactorial_lt_pow {n : ℕ} (hn : n ≠ 0) {k : ℕ} :
2 ≤ k → n.descFactorial k < n ^ k
source
theorem Nat.factorial_two_mul_le (n : ℕ) :
(2 * n).factorial ≤ (2 * n) ^ n * n.factorial
source
theorem Nat.two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) :
2 ^ n * n.factorial ≤ (2 * n).factorial

### Factorial via binary splitting. #

We prove this is equal to the standard factorial and mark it `@[csimp]`.

We could proceed further, with either Legendre or Luschny methods.

This is the highest factorial I can `#eval` using the naive implementation without a stack overflow:

    /-- info: 114716 -/
    #guard_msgs in
    #eval 9718 ! |>.log2

We could implement a tail-recursive version (or just use `Nat.fold`), but instead let's jump straight to binary splitting.

source
def Nat.factorialBinarySplitting (n : ℕ) :
ℕ

Factorial implemented using binary splitting.

While this still performs the same number of multiplications, the big-integer operands to each are much smaller.

Equations

- n.factorialBinarySplitting = if x : n = 0 then 1 else Nat.factorialBinarySplitting.prodRange 1 (n + 1) ⋯

Instances For

source
@[irreducible]
def Nat.factorialBinarySplitting.prodRange (lo hi : ℕ) (h : lo < hi := by grind) :
ℕ

`prodRange lo hi` is the product of the range `lo` to `hi` (exclusive), computed by binary splitting.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[irreducible]
theorem Nat.factorialBinarySplitting.factorial_mul_prodRange (lo hi : ℕ) (h : lo < hi) :
lo.factorial * prodRange (lo + 1) (hi + 1) ⋯ = hi.factorial
source
@[csimp]
theorem Nat.factorialBinarySplitting_eq_factorial :
factorial = factorialBinarySplitting

We are now limited by time, not stack space, and this is much faster than even the tail-recursive version.

    #time -- Less than 1s. (Tail-recursive version takes longer for `(10^5) !`.)
    #eval (10^6) ! |>.log2