# mathlib3documentation

data.nat.factorial.basic

# Factorial and variants #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the factorial, along with the ascending and descending variants.

## Main declarations #

• nat.factorial: The factorial.
• nat.asc_factorial: The ascending factorial. Note that it runs from n + 1 to n + k and not from n to n + k - 1. We might want to change that in the future.
• nat.desc_factorial: The descending factorial. It runs from n - k to n.
@[simp]
def nat.factorial  :

nat.factorial n is the factorial of n.

Equations
@[simp]
theorem nat.factorial_zero  :
@[simp]
theorem nat.factorial_succ (n : ) :
@[simp]
theorem nat.factorial_one  :
@[simp]
theorem nat.factorial_two  :
theorem nat.mul_factorial_pred {n : } (hn : 0 < n) :
n * (n - 1).factorial = n.factorial
theorem nat.factorial_pos (n : ) :
theorem nat.factorial_dvd_factorial {m n : } (h : m n) :
theorem nat.dvd_factorial {m n : } :
0 < m m n m n.factorial
theorem nat.factorial_le {m n : } (h : m n) :
theorem nat.factorial_lt {m n : } (hn : 0 < n) :
n < m
theorem nat.one_lt_factorial {n : } :
1 < n.factorial 1 < n
theorem nat.factorial_eq_one {n : } :
n.factorial = 1 n 1
theorem nat.factorial_inj {m n : } (hn : 1 < n.factorial) :
n = m
theorem nat.lt_factorial_self {n : } (hi : 3 n) :
theorem nat.add_factorial_succ_lt_factorial_add_succ {i : } (n : ) (hi : 2 i) :
i + (n + 1).factorial < (i + n + 1).factorial
theorem nat.add_factorial_lt_factorial_add {i n : } (hi : 2 i) (hn : 1 n) :
i + n.factorial < (i + n).factorial
theorem nat.add_factorial_le_factorial_add (i : ) {n : } (n1 : 1 n) :
theorem nat.factorial_mul_pow_sub_le_factorial {n m : } (hnm : n m) :
n.factorial * n ^ (m - n) m.factorial

### Ascending and descending factorials #

def nat.asc_factorial (n : ) :

n.asc_factorial k = (n + k)! / n! (as seen in nat.asc_factorial_eq_div), but implemented recursively to allow for "quick" computation when using norm_num. This is closely related to pochhammer, but much less general.

Equations
@[simp]
theorem nat.asc_factorial_zero (n : ) :
= 1
@[simp]
theorem nat.zero_asc_factorial (k : ) :
theorem nat.asc_factorial_succ {n k : } :
= (n + k + 1) *
theorem nat.succ_asc_factorial (n k : ) :
(n + 1) * = (n + k + 1) *

n.asc_factorial k = (n + k)! / n! but without ℕ-division. See nat.asc_factorial_eq_div for the version with ℕ-division.

theorem nat.asc_factorial_eq_div (n k : ) :

Avoid in favor of nat.factorial_mul_asc_factorial if you can. ℕ-division isn't worth it.

theorem nat.asc_factorial_of_sub {n k : } (h : k < n) :
(n - k) * (n - k).asc_factorial k = (n - (k + 1)).asc_factorial (k + 1)
theorem nat.pow_succ_le_asc_factorial (n k : ) :
(n + 1) ^ k
theorem nat.pow_lt_asc_factorial' (n k : ) :
(n + 1) ^ (k + 2) < n.asc_factorial (k + 2)
theorem nat.pow_lt_asc_factorial (n : ) {k : } :
2 k (n + 1) ^ k <
theorem nat.asc_factorial_le_pow_add (n k : ) :
(n + k) ^ k
theorem nat.asc_factorial_lt_pow_add (n : ) {k : } :
2 k < (n + k) ^ k
theorem nat.asc_factorial_pos (n k : ) :
0 <
def nat.desc_factorial (n : ) :

n.desc_factorial k = n! / (n - k)! (as seen in nat.desc_factorial_eq_div), but implemented recursively to allow for "quick" computation when using norm_num. This is closely related to pochhammer, but much less general.

Equations
@[simp]
theorem nat.desc_factorial_zero (n : ) :
= 1
@[simp]
theorem nat.desc_factorial_succ (n k : ) :
= (n - k) *
@[simp]
theorem nat.desc_factorial_one (n : ) :
= n
@[simp]
theorem nat.succ_desc_factorial_succ (n k : ) :
(n + 1).desc_factorial (k + 1) = (n + 1) *
theorem nat.succ_desc_factorial (n k : ) :
(n + 1 - k) * (n + 1).desc_factorial k = (n + 1) *
@[simp]
theorem nat.desc_factorial_eq_zero_iff_lt {n k : } :
= 0 n < k
theorem nat.desc_factorial_of_lt {n k : } :
n < k = 0

Alias of the reverse direction of nat.desc_factorial_eq_zero_iff_lt.

n.desc_factorial k = n! / (n - k)! but without ℕ-division. See nat.desc_factorial_eq_div for the version using ℕ-division.

theorem nat.desc_factorial_eq_div {n k : } (h : k n) :

Avoid in favor of nat.factorial_mul_desc_factorial if you can. ℕ-division isn't worth it.

theorem nat.pow_sub_le_desc_factorial (n k : ) :
(n + 1 - k) ^ k
theorem nat.pow_sub_lt_desc_factorial' {n k : } :
k + 2 n (n - (k + 1)) ^ (k + 2) < n.desc_factorial (k + 2)
theorem nat.pow_sub_lt_desc_factorial {n k : } :
2 k k n (n + 1 - k) ^ k <
theorem nat.desc_factorial_le_pow (n k : ) :
n ^ k
theorem nat.desc_factorial_lt_pow {n : } (hn : 1 n) {k : } :
2 k < n ^ k