mathlib documentation

data.nat.factorial

The factorial function #

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.succ) * n!
source
@[simp]
theorem nat.factorial_one  :
1! = 1
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 : ℕ} (h0 : 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 : ℕ} (h0 : 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)!