doubleFactorial_two_mul

Mathlib.Data.Nat.Factorial.DoubleFactorial

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

← MathLib Explorer

English

For all n, (2n)‼ = 2^n · n!.

Русский

Для всех n: (2n)‼ = 2^n · n!).

LaTeX

$$$ (2n)‼ = 2^n \cdot n! $$$

Lean4

theorem doubleFactorial_two_mul : ∀ n : ℕ, (2 * n)‼ = 2 ^ n * n !
  | 0 => rfl
  | n + 1 =>
    by
    rw [mul_add, mul_one, doubleFactorial_add_two, factorial, pow_succ, doubleFactorial_two_mul _, succ_eq_add_one]
    ring

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

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

Разделы

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

Аффилиация

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