superFactorial_zero

Mathlib.Data.Nat.Factorial.SuperFactorial

URI: https://scilib.ai/kg/mathlib#Nat.superFactorial_zero

English

The superfactorial is defined by sf 0 = 1 and sf(succ n) = factorial(n.succ) · sf n.

Русский

Суперфакториал задаётся как sf 0 = 1 и sf(Succ n) = (n+1)! · sf n.

LaTeX

$$sf(0) = 1,\; sf(n+1) = (n+1)! \cdot sf(n)$$

Lean4

@[simp]
theorem superFactorial_zero : sf 0 = 1 :=
  rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru