mathlib documentation

data.nat.factorial.basic

Factorial and variants #

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

Main declarations #

source
@[simp]
def nat.factorial  :
ℕ → ℕ

nat.factorial n is the factorial of n.

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

Ascending and descending factorials #

source
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
source
@[simp]
theorem nat.asc_factorial_zero (n : ℕ) :
n.asc_factorial 0 = 1
source
@[simp]
theorem nat.zero_asc_factorial (k : ℕ) :
0.asc_factorial k = k!
source
theorem nat.asc_factorial_succ {n k : ℕ} :
n.asc_factorial k.succ = (n + k + 1) * n.asc_factorial k
source
theorem nat.succ_asc_factorial (n k : ℕ) :
(n + 1) * n.succ.asc_factorial k = (n + k + 1) * n.asc_factorial k
source
theorem nat.factorial_mul_asc_factorial (n k : ℕ) :
n! * n.asc_factorial k = (n + k)!

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

source
theorem nat.asc_factorial_eq_div (n k : ℕ) :
n.asc_factorial k = (n + k)! / n!

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

source
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)
source
theorem nat.pow_succ_le_asc_factorial (n k : ℕ) :
(n + 1) ^ k ≤ n.asc_factorial k
source
theorem nat.pow_lt_asc_factorial' (n k : ℕ) :
(n + 1) ^ (k + 2) < n.asc_factorial (k + 2)
source
theorem nat.pow_lt_asc_factorial (n : ℕ) {k : ℕ} :
2 ≤ k → (n + 1) ^ k < n.asc_factorial k
source
theorem nat.asc_factorial_le_pow_add (n k : ℕ) :
n.asc_factorial k ≤ (n + k) ^ k
source
theorem nat.asc_factorial_lt_pow_add (n : ℕ) {k : ℕ} :
2 ≤ k → n.asc_factorial k < (n + k) ^ k
source
theorem nat.asc_factorial_pos (n k : ℕ) :
0 < n.asc_factorial k
source
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
source
@[simp]
theorem nat.desc_factorial_zero (n : ℕ) :
n.desc_factorial 0 = 1
source
@[simp]
theorem nat.desc_factorial_succ (n k : ℕ) :
n.desc_factorial k.succ = (n - k) * n.desc_factorial k
source
theorem nat.zero_desc_factorial_succ (k : ℕ) :
0.desc_factorial k.succ = 0
source
@[simp]
theorem nat.desc_factorial_one (n : ℕ) :
n.desc_factorial 1 = n
source
@[simp]
theorem nat.succ_desc_factorial_succ (n k : ℕ) :
(n + 1).desc_factorial (k + 1) = (n + 1) * n.desc_factorial k
source
theorem nat.succ_desc_factorial (n k : ℕ) :
(n + 1 - k) * (n + 1).desc_factorial k = (n + 1) * n.desc_factorial k
source
theorem nat.desc_factorial_self (n : ℕ) :
n.desc_factorial n = n!
source
@[simp]
theorem nat.desc_factorial_eq_zero_iff_lt {n k : ℕ} :
n.desc_factorial k = 0 ↔ n < k
source
theorem nat.desc_factorial_of_lt {n k : ℕ} :
n < k → n.desc_factorial k = 0

Alias of nat.desc_factorial_eq_zero_iff_lt.

source
theorem nat.add_desc_factorial_eq_asc_factorial (n k : ℕ) :
(n + k).desc_factorial k = n.asc_factorial k
source
theorem nat.factorial_mul_desc_factorial {n k : ℕ} :
k ≤ n → (n - k)! * n.desc_factorial k = n!

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

source
theorem nat.desc_factorial_eq_div {n k : ℕ} (h : k ≤ n) :
n.desc_factorial k = n! / (n - k)!

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

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