add_choose_mul_factorial_mul_factorial

Mathlib.Data.Nat.Choose.Basic

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

← MathLib Explorer

English

For i,j ∈ ℕ, C(i+j,j) · i! · j! = (i+j)!.

Русский

Для любых i,j ∈ ℕ: C(i+j,j) i! j! = (i+j)!.

LaTeX

$$$\\\\binom{i+j}{j} \\\\cdot i! \\\\cdot j! = (i+j)!\$$$

Lean4

theorem add_choose_mul_factorial_mul_factorial (i j : ℕ) : (i + j).choose j * i ! * j ! = (i + j)! := by
  rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), Nat.add_sub_cancel_right, Nat.mul_right_comm]

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

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

Разделы

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

Аффилиация

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