mathlib documentation

data.nat.fact

The factorial function

source
@[simp]
def nat.fact (a : ℕ) :
ℕ

nat.fact n is the factorial of n.

Equations
source
@[simp]
theorem nat.fact_zero  :
0.fact = 1

source
@[simp]
theorem nat.fact_succ (n : ℕ) :
n.succ.fact = (n.succ) * n.fact

source
@[simp]
theorem nat.fact_one  :
1.fact = 1

source
theorem nat.fact_pos (n : ℕ) :
0 < n.fact

source
theorem nat.fact_ne_zero (n : ℕ) :
n.fact ≠ 0

source
theorem nat.fact_dvd_fact {m n : ℕ} (h : m ≤ n) :
m.fact ∣ n.fact

source
theorem nat.dvd_fact {m n : ℕ} (a : 0 < m) (a_1 : m ≤ n) :
m ∣ n.fact

source
theorem nat.fact_le {m n : ℕ} (h : m ≤ n) :
m.fact ≤ n.fact

source
theorem nat.fact_mul_pow_le_fact {m n : ℕ} :
(m.fact) * m.succ ^ n ≤ (m + n).fact

source
theorem nat.monotone_fact  :
monotone nat.fact

source
theorem nat.fact_lt {m n : ℕ} (h0 : 0 < n) :
n.fact < m.fact ↔ n < m

source
theorem nat.one_lt_fact {n : ℕ} :
1 < n.fact ↔ 1 < n

source
theorem nat.fact_eq_one {n : ℕ} :
n.fact = 1 ↔ n ≤ 1

source
theorem nat.fact_inj {m n : ℕ} (h0 : 1 < n.fact) :
n.fact = m.fact ↔ n = m