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.

Equations

• Nat.superFactorial 0 = 1
• Nat.superFactorial (Nat.succ n) = Nat.factorial (Nat.succ n) * Nat.superFactorial n

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

@[simp]

theorem Nat.superFactorial_zero : Nat.superFactorial 0 = 1

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

@[simp]

theorem Nat.superFactorial_one : Nat.superFactorial 1 = 1

@[simp]

theorem Nat.superFactorial_two : Nat.superFactorial 2 = 2

@[simp]

theorem Nat.prod_Icc_factorial (n : ℕ) : (Finset.prod (Finset.Icc 1 n) fun (x : ℕ) => Nat.factorial x) = Nat.superFactorial n

@[simp]

theorem Nat.prod_range_factorial_succ (n : ℕ) : (Finset.prod (Finset.range n) fun (x : ℕ) => Nat.factorial (x + 1)) = Nat.superFactorial n

@[simp]

theorem Nat.prod_range_succ_factorial (n : ℕ) : (Finset.prod (Finset.range (n + 1)) fun (x : ℕ) => Nat.factorial x) = Nat.superFactorial n

theorem Nat.det_vandermonde_id_eq_superFactorial {R : Type u_1} [CommRing R] (n : ℕ) : Matrix.det (Matrix.vandermonde fun (i : Fin (n + 1)) => ↑↑i) = ↑(Nat.superFactorial n)

theorem Nat.superFactorial_two_mul (n : ℕ) : Nat.superFactorial (2 * n) = (Finset.prod (Finset.range n) fun (i : ℕ) => Nat.factorial (2 * i + 1)) ^ 2 * 2 ^ n * Nat.factorial n

theorem Nat.superFactorial_four_mul (n : ℕ) : Nat.superFactorial (4 * n) = ((Finset.prod (Finset.range (2 * n)) fun (i : ℕ) => Nat.factorial (2 * i + 1)) * 2 ^ n) ^ 2 * Nat.factorial (2 * n)

theorem Nat.superFactorial_dvd_vandermonde_det {n : ℕ} (v : Fin (n + 1) → ℤ) : ↑(Nat.superFactorial n) ∣ Matrix.det (Matrix.vandermonde v)