mathlib documentation

data.nat.factorial

The factorial function

@[simp]
def nat.factorial  :

nat.factorial n is the factorial of n.

Equations
@[simp]
theorem nat.factorial_zero  :
0! = 1!

@[simp]
theorem nat.factorial_succ (n : ) :
(n.succ)! = (n.succ) * n!

@[simp]
theorem nat.factorial_one  :
1! = 1

theorem nat.mul_factorial_pred {n : } (hn : 0 < n) :
n * (n - 1)! = n!

theorem nat.factorial_pos (n : ) :
0 < n!

theorem nat.factorial_ne_zero (n : ) :
n! 0

theorem nat.factorial_dvd_factorial {m n : } (h : m n) :
m! n!

theorem nat.dvd_factorial {m n : } :
0 < mm nm n!

theorem nat.factorial_le {m n : } (h : m n) :
m! n!

theorem nat.factorial_mul_pow_le_factorial {m n : } :
m! * m.succ ^ n (m + n)!

theorem nat.factorial_lt {m n : } (h0 : 0 < n) :
n! < m! n < m

theorem nat.one_lt_factorial {n : } :
1 < n! 1 < n

theorem nat.factorial_eq_one {n : } :
n! = 1 n 1

theorem nat.factorial_inj {m n : } (h0 : 1 < n!) :
n! = m! n = m

theorem nat.self_le_factorial (n : ) :
n n!