factorial_eq_mul_doubleFactorial

Mathlib.Data.Nat.Factorial.DoubleFactorial

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

← MathLib Explorer

English

For all n, (n+1)! = (n+1)‼ · n‼.

Русский

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

LaTeX

$$$ (n+1)! = (n+1)‼ \cdot n‼ $$$

Lean4

theorem factorial_eq_mul_doubleFactorial : ∀ n : ℕ, (n + 1)! = (n + 1)‼ * n‼
  | 0 => rfl
  | k + 1 => by rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼, mul_assoc]

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

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

Разделы

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

Аффилиация

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