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 n is the factorial of n.

Equations
Instances For

    factorial notation n!

    Equations
    Instances For
      theorem Nat.factorial_succ (n : ) :
      (n + 1).factorial = (n + 1) * n.factorial
      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 < mm nm 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
      Instances For
        @[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
        @[simp]
        theorem Nat.one_ascFactorial (k : ) :
        Nat.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
        Instances For
          @[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.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 < kn.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 kk 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 kn.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