# Documentation

Mathlib.Data.Nat.Factorial.Basic

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

Nat.factorial n is the factorial of n.

Equations
Instances For

factorial notation n!

Instances For
@[simp]
theorem Nat.factorial_succ (n : ) :
= (n + 1) *
theorem Nat.mul_factorial_pred {n : } (hn : 0 < n) :
n * Nat.factorial (n - 1) =
theorem Nat.factorial_dvd_factorial {m : } {n : } (h : m n) :
theorem Nat.dvd_factorial {m : } {n : } :
0 < mm n
theorem Nat.factorial_le {m : } {n : } (h : m n) :
theorem Nat.factorial_le_of_le {m : } {n : } (h : n m) :
theorem Nat.factorial_lt {m : } {n : } (hn : 0 < n) :
n < m
theorem Nat.factorial_lt_of_lt {m : } {n : } (hn : 0 < n) (h : n < m) :
theorem Nat.one_lt_factorial {n : } :
1 < n
theorem Nat.factorial_inj {m : } {n : } (hn : ) :
n = m
theorem Nat.lt_factorial_self {n : } (hi : 3 n) :
theorem Nat.add_factorial_lt_factorial_add {i : } {n : } (hi : 2 i) (hn : 1 n) :
theorem Nat.add_factorial_le_factorial_add (i : ) {n : } (n1 : 1 n) :
theorem Nat.factorial_mul_pow_sub_le_factorial {n : } {m : } (hnm : n m) :
* n ^ (m - n)

### 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
Instances For
@[simp]
theorem Nat.ascFactorial_zero (n : ) :
= 1
@[simp]
theorem Nat.zero_ascFactorial (k : ) :
theorem Nat.ascFactorial_succ {n : } {k : } :
= (n + k + 1) *
theorem Nat.succ_ascFactorial (n : ) (k : ) :
(n + 1) * = (n + k + 1) *

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

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
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 <
theorem Nat.ascFactorial_le_pow_add (n : ) (k : ) :
(n + k) ^ k
theorem Nat.ascFactorial_lt_pow_add (n : ) {k : } :
2 k < (n + k) ^ k
theorem Nat.ascFactorial_pos (n : ) (k : ) :
0 <
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
Instances For
@[simp]
theorem Nat.descFactorial_zero (n : ) :
= 1
@[simp]
theorem Nat.descFactorial_succ (n : ) (k : ) :
= (n - k) *
theorem Nat.succ_descFactorial_succ (n : ) (k : ) :
Nat.descFactorial (n + 1) (k + 1) = (n + 1) *
theorem Nat.succ_descFactorial (n : ) (k : ) :
(n + 1 - k) * Nat.descFactorial (n + 1) k = (n + 1) *
@[simp]
theorem Nat.descFactorial_eq_zero_iff_lt {n : } {k : } :
= 0 n < k
theorem Nat.descFactorial_of_lt {n : } {k : } :
n < k = 0

Alias of the reverse direction of Nat.descFactorial_eq_zero_iff_lt.

theorem Nat.factorial_mul_descFactorial {n : } {k : } :
k nNat.factorial (n - k) * =

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) :

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
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 kk n(n + 1 - k) ^ k <
theorem Nat.descFactorial_le_pow (n : ) (k : ) :
n ^ k
theorem Nat.descFactorial_lt_pow {n : } (hn : 1 n) {k : } :
2 k < n ^ k