doubleFactorial

Mathlib.Data.Nat.Factorial.DoubleFactorial

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

← MathLib Explorer

English

Define the double factorial by 0!! = 1, 1!! = 1, and (k+2)!! = (k+2)·k!!.

Русский

Определение двойного факториала: 0!! = 1, 1!! = 1, и (k+2)!! = (k+2)·k!!.

LaTeX

$$$0!! = 1,\; 1!! = 1,\; (k+2)!! = (k+2) \cdot k!! $$$

Lean4

/-- `Nat.doubleFactorial n` is the double factorial of `n`. -/
@[simp]
def doubleFactorial : ℕ → ℕ
  | 0 => 1
  | 1 => 1
  | k + 2 => (k + 2) * doubleFactorial k

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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