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

    Instances For
      source
      @[simp]
      theorem Nat.superFactorial_zero :
      Nat.superFactorial 0 = 1
      source
      theorem Nat.superFactorial_succ (n : ℕ) :
      Nat.superFactorial (Nat.succ n) = Nat.factorial (n + 1) * Nat.superFactorial n
      source
      @[simp]
      theorem Nat.superFactorial_one :
      Nat.superFactorial 1 = 1
      source
      @[simp]
      theorem Nat.superFactorial_two :
      Nat.superFactorial 2 = 2
      source
      theorem Nat.det_vandermonde_id_eq_superFactorial {R : Type u_1} [CommRing R] (n : ℕ) :
      Matrix.det (Matrix.vandermonde fun i => ↑↑i) = ↑(Nat.superFactorial n)