Factorial and variants

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

Main declarations

• Nat.factorial: The factorial.
• Nat.ascFactorial: 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.descFactorial: The descending factorial. It runs from n - k to n.

def Nat.factorial : ℕ → ℕ

Nat.factorial n is the factorial of n.

Equations

• Nat.factorial 0 = 1
• Nat.factorial (Nat.succ n) = Nat.succ n * Nat.factorial n

def Nat.term_! : Lean.TrailingParserDescr

factorial notation n!

Equations

• Nat.term_! = Lean.ParserDescr.trailingNode `Nat.term_! 10000 0 (Lean.ParserDescr.symbol "!")

@[simp]

theorem Nat.factorial_zero : Nat.factorial 0 = 1

theorem Nat.factorial_succ (n : ℕ) : Nat.factorial (Nat.succ n) = (n + 1) * Nat.factorial n

theorem Nat.factorial_one : Nat.factorial 1 = 1

theorem Nat.factorial_two : Nat.factorial 2 = 2

theorem Nat.mul_factorial_pred {n : ℕ} (hn : 0 < n) : n * Nat.factorial (n - 1) = Nat.factorial n

theorem Nat.factorial_pos (n : ℕ) : 0 < Nat.factorial n

theorem Nat.factorial_ne_zero (n : ℕ) : Nat.factorial n ≠ 0

theorem Nat.factorial_dvd_factorial {m : ℕ} {n : ℕ} (h : m ≤ n) : Nat.factorial m ∣ Nat.factorial n

theorem Nat.dvd_factorial {m : ℕ} {n : ℕ} : 0 < m → m ≤ n → m ∣ Nat.factorial n

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

theorem Nat.factorial_mul_pow_le_factorial {m : ℕ} {n : ℕ} : Nat.factorial m * Nat.succ m ^ n ≤ Nat.factorial (m + n)

theorem Nat.monotone_factorial : Monotone Nat.factorial

theorem Nat.factorial_le_of_le {m : ℕ} {n : ℕ} (h : n ≤ m) : Nat.factorial n ≤ Nat.factorial m

theorem Nat.factorial_lt {m : ℕ} {n : ℕ} (hn : 0 < n) : Nat.factorial n < Nat.factorial m ↔ n < m

theorem Nat.factorial_lt_of_lt {m : ℕ} {n : ℕ} (hn : 0 < n) (h : n < m) : Nat.factorial n < Nat.factorial m

theorem Nat.one_lt_factorial {n : ℕ} : 1 < Nat.factorial n ↔ 1 < n

theorem Nat.factorial_eq_one {n : ℕ} : Nat.factorial n = 1 ↔ n ≤ 1

theorem Nat.factorial_inj {m : ℕ} {n : ℕ} (hn : 1 < Nat.factorial n) : Nat.factorial n = Nat.factorial m ↔ n = m

theorem Nat.self_le_factorial (n : ℕ) : n ≤ Nat.factorial n

theorem Nat.lt_factorial_self {n : ℕ} (hi : 3 ≤ n) : n < Nat.factorial n

theorem Nat.add_factorial_succ_lt_factorial_add_succ {i : ℕ} (n : ℕ) (hi : 2 ≤ i) : i + Nat.factorial (n + 1) < Nat.factorial (i + n + 1)

theorem Nat.add_factorial_lt_factorial_add {i : ℕ} {n : ℕ} (hi : 2 ≤ i) (hn : 1 ≤ n) : i + Nat.factorial n < Nat.factorial (i + n)

theorem Nat.add_factorial_succ_le_factorial_add_succ (i : ℕ) (n : ℕ) : i + Nat.factorial (n + 1) ≤ Nat.factorial (i + (n + 1))

theorem Nat.add_factorial_le_factorial_add (i : ℕ) {n : ℕ} (n1 : 1 ≤ n) : i + Nat.factorial n ≤ Nat.factorial (i + n)

theorem Nat.factorial_mul_pow_sub_le_factorial {n : ℕ} {m : ℕ} (hnm : n ≤ m) : Nat.factorial n * n ^ (m - n) ≤ Nat.factorial m

Ascending and descending factorials

def Nat.ascFactorial (n : ℕ) : ℕ → ℕ

n.ascFactorial k = (n + k)! / n! (as seen in Nat.ascFactorial_eq_div), but implemented recursively to allow for "quick" computation when using norm_num. This is closely related to ascPochhammer, but much less general.

Equations

• Nat.ascFactorial n 0 = 1
• Nat.ascFactorial n (Nat.succ n_1) = (n + n_1 + 1) * Nat.ascFactorial n n_1

@[simp]

theorem Nat.ascFactorial_zero (n : ℕ) : Nat.ascFactorial n 0 = 1

@[simp]

theorem Nat.zero_ascFactorial (k : ℕ) : Nat.ascFactorial 0 k = Nat.factorial k

theorem Nat.ascFactorial_succ {n : ℕ} {k : ℕ} : Nat.ascFactorial n (Nat.succ k) = (n + k + 1) * Nat.ascFactorial n k

theorem Nat.succ_ascFactorial (n : ℕ) (k : ℕ) : (n + 1) * Nat.ascFactorial (Nat.succ n) k = (n + k + 1) * Nat.ascFactorial n k

theorem Nat.factorial_mul_ascFactorial (n : ℕ) (k : ℕ) : Nat.factorial n * Nat.ascFactorial n k = Nat.factorial (n + k)

n.ascFactorial k = (n + k)! / n! but without ℕ-division. See Nat.ascFactorial_eq_div for the version with ℕ-division.

theorem Nat.ascFactorial_eq_div (n : ℕ) (k : ℕ) : Nat.ascFactorial n k = Nat.factorial (n + k) / Nat.factorial n

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

theorem Nat.ascFactorial_of_sub {n : ℕ} {k : ℕ} (h : k < n) : (n - k) * Nat.ascFactorial (n - k) k = Nat.ascFactorial (n - (k + 1)) (k + 1)

theorem Nat.pow_succ_le_ascFactorial (n : ℕ) (k : ℕ) : (n + 1) ^ k ≤ Nat.ascFactorial n k

theorem Nat.pow_lt_ascFactorial' (n : ℕ) (k : ℕ) : (n + 1) ^ (k + 2) < Nat.ascFactorial n (k + 2)

theorem Nat.pow_lt_ascFactorial (n : ℕ) {k : ℕ} : 2 ≤ k → (n + 1) ^ k < Nat.ascFactorial n k

theorem Nat.ascFactorial_le_pow_add (n : ℕ) (k : ℕ) : Nat.ascFactorial n k ≤ (n + k) ^ k

theorem Nat.ascFactorial_lt_pow_add (n : ℕ) {k : ℕ} : 2 ≤ k → Nat.ascFactorial n k < (n + k) ^ k

theorem Nat.ascFactorial_pos (n : ℕ) (k : ℕ) : 0 < Nat.ascFactorial n k

def Nat.descFactorial (n : ℕ) : ℕ → ℕ

n.descFactorial k = n! / (n - k)! (as seen in Nat.descFactorial_eq_div), but implemented recursively to allow for "quick" computation when using norm_num. This is closely related to ascPochhammer, but much less general.

Equations

• Nat.descFactorial n 0 = 1
• Nat.descFactorial n (Nat.succ n_1) = (n - n_1) * Nat.descFactorial n n_1

@[simp]

theorem Nat.descFactorial_zero (n : ℕ) : Nat.descFactorial n 0 = 1

@[simp]

theorem Nat.descFactorial_succ (n : ℕ) (k : ℕ) : Nat.descFactorial n (Nat.succ k) = (n - k) * Nat.descFactorial n k

theorem Nat.zero_descFactorial_succ (k : ℕ) : Nat.descFactorial 0 (Nat.succ k) = 0

theorem Nat.descFactorial_one (n : ℕ) : Nat.descFactorial n 1 = n

theorem Nat.succ_descFactorial_succ (n : ℕ) (k : ℕ) : Nat.descFactorial (n + 1) (k + 1) = (n + 1) * Nat.descFactorial n k

theorem Nat.succ_descFactorial (n : ℕ) (k : ℕ) : (n + 1 - k) * Nat.descFactorial (n + 1) k = (n + 1) * Nat.descFactorial n k

theorem Nat.descFactorial_self (n : ℕ) : Nat.descFactorial n n = Nat.factorial n

@[simp]

theorem Nat.descFactorial_eq_zero_iff_lt {n : ℕ} {k : ℕ} : Nat.descFactorial n k = 0 ↔ n < k

theorem Nat.descFactorial_of_lt {n : ℕ} {k : ℕ} : n < k → Nat.descFactorial n k = 0

Alias of the reverse direction of Nat.descFactorial_eq_zero_iff_lt.

theorem Nat.add_descFactorial_eq_ascFactorial (n : ℕ) (k : ℕ) : Nat.descFactorial (n + k) k = Nat.ascFactorial n k

theorem Nat.factorial_mul_descFactorial {n : ℕ} {k : ℕ} : k ≤ n → Nat.factorial (n - k) * Nat.descFactorial n k = Nat.factorial n

n.descFactorial k = n! / (n - k)! but without ℕ-division. See Nat.descFactorial_eq_div for the version using ℕ-division.

theorem Nat.descFactorial_eq_div {n : ℕ} {k : ℕ} (h : k ≤ n) : Nat.descFactorial n k = Nat.factorial n / Nat.factorial (n - k)

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

theorem Nat.pow_sub_le_descFactorial (n : ℕ) (k : ℕ) : (n + 1 - k) ^ k ≤ Nat.descFactorial n k

theorem Nat.pow_sub_lt_descFactorial' {n : ℕ} {k : ℕ} : k + 2 ≤ n → (n - (k + 1)) ^ (k + 2) < Nat.descFactorial n (k + 2)

theorem Nat.pow_sub_lt_descFactorial {n : ℕ} {k : ℕ} : 2 ≤ k → k ≤ n → (n + 1 - k) ^ k < Nat.descFactorial n k

theorem Nat.descFactorial_le_pow (n : ℕ) (k : ℕ) : Nat.descFactorial n k ≤ n ^ k

theorem Nat.descFactorial_lt_pow {n : ℕ} (hn : 1 ≤ n) {k : ℕ} : 2 ≤ k → Nat.descFactorial n k < n ^ k