Documentation

Mathlib.Data.Nat.Factorial.SuperFactorial

Superfactorial #

This file defines the superfactorial sf n = 1! * 2! * 3! * ... * n!.

Main declarations #

source
def Nat.superFactorial :
ℕ → ℕ

Nat.superFactorial n is the superfactorial of n.

Equations
Instances For
    source
    def Nat.termSf_ :
    Lean.ParserDescr

    sf notation for superfactorial

    Equations
    Instances For
      source
      @[simp]
      theorem Nat.superFactorial_zero :
      Nat.superFactorial 0 = 1
      source
      theorem Nat.superFactorial_succ (n : ℕ) :
      n.succ.superFactorial = (n + 1).factorial * n.superFactorial
      source
      @[simp]
      theorem Nat.superFactorial_one :
      Nat.superFactorial 1 = 1
      source
      @[simp]
      theorem Nat.superFactorial_two :
      Nat.superFactorial 2 = 2
      source
      @[simp]
      theorem Nat.prod_Icc_factorial (n : ℕ) :
      ∏ x ∈ Finset.Icc 1 n, x.factorial = n.superFactorial
      source
      @[simp]
      theorem Nat.prod_range_factorial_succ (n : ℕ) :
      ∏ x ∈ Finset.range n, (x + 1).factorial = n.superFactorial
      source
      @[simp]
      theorem Nat.prod_range_succ_factorial (n : ℕ) :
      ∏ x ∈ Finset.range (n + 1), x.factorial = n.superFactorial
      source
      theorem Nat.det_vandermonde_id_eq_superFactorial {R : Type u_1} [CommRing R] (n : ℕ) :
      (Matrix.vandermonde fun (i : Fin (n + 1)) => ↑↑i).det = ↑n.superFactorial
      source
      theorem Nat.superFactorial_two_mul (n : ℕ) :
      (2 * n).superFactorial = (∏ i ∈ Finset.range n, (2 * i + 1).factorial) ^ 2 * 2 ^ n * n.factorial
      source
      theorem Nat.superFactorial_four_mul (n : ℕ) :
      (4 * n).superFactorial = ((∏ i ∈ Finset.range (2 * n), (2 * i + 1).factorial) * 2 ^ n) ^ 2 * (2 * n).factorial
      source
      theorem Nat.superFactorial_dvd_vandermonde_det {n : ℕ} (v : Fin (n + 1) → ℤ) :
      ↑n.superFactorial ∣ (Matrix.vandermonde v).det