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.

source

@[simp]

def nat.factorial :

ℕ → ℕ

nat.factorial n is the factorial of n.

Equations

n.succ.factorial = n.succ * n.factorial
0.factorial = 1

source

@[simp]

theorem nat.factorial_zero :

0.factorial = 1

source

@[simp]

theorem nat.factorial_succ (n : ℕ) :

n.succ.factorial = (n + 1) * n.factorial

source

@[simp]

theorem nat.factorial_one :

1.factorial = 1

source

@[simp]

theorem nat.factorial_two :

2.factorial = 2

source

theorem nat.mul_factorial_pred {n : ℕ} (hn : 0 < n) :

n * (n - 1).factorial = n.factorial

source

theorem nat.factorial_pos (n : ℕ) :

0 < n.factorial

source

theorem nat.factorial_ne_zero (n : ℕ) :

n.factorial ≠ 0

source

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

m.factorial ∣ n.factorial

source

theorem nat.dvd_factorial {m n : ℕ} :

0 < m → m ≤ n → m ∣ n.factorial

source

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

m.factorial ≤ n.factorial

source

theorem nat.factorial_mul_pow_le_factorial {m n : ℕ} :

m.factorial * m.succ ^ n ≤ (m + n).factorial

source

theorem nat.monotone_factorial :

monotone nat.factorial

source

theorem nat.factorial_lt {m n : ℕ} (hn : 0 < n) :

n.factorial < m.factorial ↔ n < m

source

theorem nat.one_lt_factorial {n : ℕ} :

1 < n.factorial ↔ 1 < n

source

theorem nat.factorial_eq_one {n : ℕ} :

n.factorial = 1 ↔ n ≤ 1

source

theorem nat.factorial_inj {m n : ℕ} (hn : 1 < n.factorial) :

n.factorial = m.factorial ↔ n = m

source

theorem nat.self_le_factorial (n : ℕ) :

n ≤ n.factorial

source

theorem nat.lt_factorial_self {n : ℕ} (hi : 3 ≤ n) :

n < n.factorial

source

theorem nat.add_factorial_succ_lt_factorial_add_succ {i : ℕ} (n : ℕ) (hi : 2 ≤ i) :

i + (n + 1).factorial < (i + n + 1).factorial

source

theorem nat.add_factorial_lt_factorial_add {i n : ℕ} (hi : 2 ≤ i) (hn : 1 ≤ n) :

i + n.factorial < (i + n).factorial

source

theorem nat.add_factorial_succ_le_factorial_add_succ (i n : ℕ) :

i + (n + 1).factorial ≤ (i + (n + 1)).factorial

source

theorem nat.add_factorial_le_factorial_add (i : ℕ) {n : ℕ} (n1 : 1 ≤ n) :

i + n.factorial ≤ (i + n).factorial

source

theorem nat.factorial_mul_pow_sub_le_factorial {n m : ℕ} (hnm : n ≤ m) :

n.factorial * n ^ (m - n) ≤ m.factorial

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

n.asc_factorial (k + 1) = (n + k + 1) * n.asc_factorial k
n.asc_factorial 0 = 1

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.factorial

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.factorial * n.asc_factorial k = (n + k).factorial

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).factorial / n.factorial

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