Documentation

Mathlib.Data.Nat.Factorial.SuperFactorial

Superfactorial #

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

Main declarations #

sf notation for superfactorial

Equations
@[simp]
@[simp]
@[simp]
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
theorem Nat.superFactorial_two_mul (n : ) :
(2 * n).superFactorial = (∏ iFinset.range n, (2 * i + 1).factorial) ^ 2 * 2 ^ n * n.factorial
theorem Nat.superFactorial_four_mul (n : ) :
(4 * n).superFactorial = ((∏ iFinset.range (2 * n), (2 * i + 1).factorial) * 2 ^ n) ^ 2 * (2 * n).factorial