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.mul_factorial_pred {n : } (hn : 0 < n) :
      theorem Nat.dvd_factorial {m : } {n : } :
      0 < mm nm Nat.factorial n
      theorem Nat.factorial_le {m : } {n : } (h : m n) :
      theorem Nat.factorial_lt {m : } {n : } (hn : 0 < n) :
      theorem Nat.factorial_lt_of_lt {m : } {n : } (hn : 0 < n) (h : n < m) :
      @[simp]
      theorem Nat.one_lt_factorial {n : } :
      @[simp]
      theorem Nat.factorial_inj {m : } {n : } (hn : 1 < n) :
      theorem Nat.factorial_inj' {m : } {n : } (h : 1 < n 1 < 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) :

      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
      Instances For
        @[simp]

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

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

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

          Alias of the reverse direction of Nat.descFactorial_eq_zero_iff_lt.

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

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