Superfactorial

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

Main declarations

• Nat.superFactorial: The superfactorial, denoted by sf.

def Nat.superFactorial : ℕ → ℕ

Nat.superFactorial n is the superfactorial of n.

def Nat.termSf_ : Lean.ParserDescr

sf notation for superfactorial

@[simp]

theorem Nat.superFactorial_zero : superFactorial 0 = 1

theorem Nat.superFactorial_succ (n : ℕ) : n.succ.superFactorial = (n + 1).factorial * n.superFactorial

@[simp]

theorem Nat.superFactorial_one : superFactorial 1 = 1

@[simp]

theorem Nat.superFactorial_two : superFactorial 2 = 2

@[simp]

theorem Nat.prod_Icc_factorial (n : ℕ) : ∏ x ∈ Finset.Icc 1 n, x.factorial = n.superFactorial

@[simp]

theorem Nat.prod_range_factorial_succ (n : ℕ) : ∏ x ∈ Finset.range n, (x + 1).factorial = n.superFactorial

@[simp]

theorem Nat.prod_range_succ_factorial (n : ℕ) : ∏ x ∈ Finset.range (n + 1), x.factorial = n.superFactorial

theorem Nat.superFactorial_two_mul (n : ℕ) : (2 * n).superFactorial = (∏ i ∈ Finset.range n, (2 * i + 1).factorial) ^ 2 * 2 ^ n * n.factorial

theorem Nat.superFactorial_four_mul (n : ℕ) : (4 * n).superFactorial = ((∏ i ∈ Finset.range (2 * n), (2 * i + 1).factorial) * 2 ^ n) ^ 2 * (2 * n).factorial