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. It is the product of natural numbers from n to n + k - 1.
• Nat.descFactorial: The descending factorial. It is the product of natural numbers from n - k + 1 to n.

def Nat.factorial : ℕ → ℕ

Nat.factorial n is the factorial of n.

Equations

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

def Nat.term_! : Lean.TrailingParserDescr

factorial notation (n)! for Nat.factorial n. In Lean, names can end with exclamation marks (e.g. List.get!), so you cannot write n! in Lean, but must write (n)! or n ! instead. The former is preferred, since Lean can confuse the ! in n ! as the (prefix) boolean negation operation in some cases. For numerals the parentheses are not required, so e.g. 0! or 1! work fine. Todo: replace occurrences of n ! with (n)! in Mathlib.

Equations

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

@[simp]

theorem Nat.factorial_zero : factorial 0 = 1

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

@[simp]

theorem Nat.factorial_one : factorial 1 = 1

@[simp]

theorem Nat.factorial_two : factorial 2 = 2

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

theorem Nat.factorial_le_pow (n : ℕ) : n.factorial ≤ n ^ n

Ascending and descending factorials

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

n.ascFactorial k = n (n + 1) ⋯ (n + k - 1). This is closely related to ascPochhammer, but much less general.

Equations

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

@[simp]

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

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

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

@[simp]

theorem Nat.one_ascFactorial (k : ℕ) : ascFactorial 1 k = k.factorial

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

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

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

theorem Nat.factorial_mul_ascFactorial' (n k : ℕ) (h : 0 < n) : (n - 1).factorial * n.ascFactorial k = (n + k - 1).factorial

n.ascFactorial k = (n + k - 1)! / (n - 1)! for n > 0 but without ℕ-division. See Nat.ascFactorial_eq_div for the version with ℕ-division. Consider using factorial_mul_ascFactorial to avoid complications of ℕ-subtraction.

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

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

theorem Nat.ascFactorial_eq_div' (n k : ℕ) (h : 0 < n) : n.ascFactorial k = (n + k - 1).factorial / (n - 1).factorial

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

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

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

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

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

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

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

theorem Nat.ascFactorial_pos (n k : ℕ) : 0 < (n + 1).ascFactorial 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 descPochhammer, but much less general.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

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

Alias of the reverse direction of Nat.descFactorial_eq_zero_iff_lt.

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

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

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

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

theorem Nat.descFactorial_mul_descFactorial {k m n : ℕ} (hkm : k ≤ m) : (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

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

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

theorem Nat.descFactorial_le (n : ℕ) {k m : ℕ} (h : k ≤ m) : k.descFactorial n ≤ m.descFactorial n

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

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

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

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

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

theorem Nat.factorial_two_mul_le (n : ℕ) : (2 * n).factorial ≤ (2 * n) ^ n * n.factorial

theorem Nat.two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) : 2 ^ n * n.factorial ≤ (2 * n).factorial