Superfactorial #
This file defines the superfactorial
sf n = 1! * 2! * 3! * ...* n!
.
Main declarations #
Nat.superFactorial
: The superfactorial, denoted bysf
.
theorem
Nat.superFactorial_succ
(n : ℕ)
:
Nat.superFactorial (Nat.succ n) = Nat.factorial (n + 1) * Nat.superFactorial n
theorem
Nat.det_vandermonde_id_eq_superFactorial
{R : Type u_1}
[CommRing R]
(n : ℕ)
:
Matrix.det (Matrix.vandermonde fun i => ↑↑i) = ↑(Nat.superFactorial n)