feat: super factorial (#6768)

Co-authored-by: Moritz Firsching <firsching@google.com>

Mathlib.lean

@@ -1632,6 +1632,7 @@ import Mathlib.Data.Nat.Factorial.Basic
 import Mathlib.Data.Nat.Factorial.BigOperators
 import Mathlib.Data.Nat.Factorial.Cast
 import Mathlib.Data.Nat.Factorial.DoubleFactorial
+import Mathlib.Data.Nat.Factorial.SuperFactorial
 import Mathlib.Data.Nat.Factorization.Basic
 import Mathlib.Data.Nat.Factorization.PrimePow
 import Mathlib.Data.Nat.Factors

Mathlib/Data/Nat/Factorial/SuperFactorial.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2023 Moritz Firsching. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Firsching
+-/
+import Mathlib.Data.Nat.Factorial.Basic
+
+/-!
+# Superfactorial
+
+This file defines the [superfactorial](https://en.wikipedia.org/wiki/Superfactorial)
+`sf n = 1! * 2! * 3! * ...* n!`.
+
+## Main declarations
+
+* `Nat.superFactorial`: The superfactorial, denoted by `sf`.
+-/
+
+
+namespace Nat
+
+/-- `Nat.superFactorial n` is the superfactorial of `n`. -/
+def superFactorial : ℕ → ℕ
+  | 0 => 1
+  | succ n => factorial n.succ * superFactorial n
+
+/-- `sf` notation for superfactorial -/
+scoped notation "sf" n:60 => Nat.superFactorial n
+
+section SuperFactorial
+
+variable {n : ℕ}
+
+@[simp]
+theorem superFactorial_zero : sf 0 = 1 :=
+  rfl
+
+theorem superFactorial_succ (n : ℕ) : (sf n.succ) = (n + 1)! * sf n :=
+  rfl
+
+@[simp]
+theorem superFactorial_one : sf 1 = 1 :=
+  rfl
+
+@[simp]
+theorem superFactorial_two : sf 2 = 2 :=
+  rfl
+
+end SuperFactorial
+
+end Nat