# Superfactorial #

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

## Main declarations #

- `Nat.superFactorial`: The superfactorial, denoted by `sf`.

source
def Nat.superFactorial :
ℕ → ℕ

`Nat.superFactorial n` is the superfactorial of `n`.

Equations

- Nat.superFactorial 0 = 1
- n.succ.superFactorial = n.succ.factorial * n.superFactorial

Instances For

source
def Nat.termSf_ :
Lean.ParserDescr

`sf` notation for superfactorial

Equations

- Nat.termSf_ = Lean.ParserDescr.node `Nat.termSf_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "sf ") (Lean.ParserDescr.cat `term 60))

Instances For

source
@[simp]
theorem Nat.superFactorial_zero :
superFactorial 0 = 1
source
theorem Nat.superFactorial_succ (n : ℕ) :
n.succ.superFactorial = (n + 1).factorial * n.superFactorial
source
@[simp]
theorem Nat.superFactorial_one :
superFactorial 1 = 1
source
@[simp]
theorem Nat.superFactorial_two :
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.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