superFactorial

Mathlib.Data.Nat.Factorial.SuperFactorial

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

English

For all n, (2n+1)‼ equals the product over i in range n of (2(i+1)+1).

Русский

Для всех n, (2n+1)‼ равно произведению по i из диапазона n от (2(i+1)+1).

LaTeX

$$$ (2n+1)‼ = \prod_{i \in \mathrm{range}(n)} (2(i+1)+1) $$$

Lean4

/-- `Nat.superFactorial n` is the superfactorial of `n`. -/
def superFactorial : ℕ → ℕ
  | 0 => 1
  | succ n => factorial n.succ * superFactorial n

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

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

Разделы

Аффилиация

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