multichoose_zero_succ

Mathlib.RingTheory.Binomial

URI: https://scilib.ai/kg/mathlib#Ring.multichoose_zero_succ

← MathLib Explorer

English

For any natural k, multichoose 0 (k+1) equals 0.

Русский

Для любого натурального k, multichoose 0 (k+1) равно 0.

LaTeX

$$$multichoose\; 0\; (k+1) = 0$$$

Lean4

@[simp]
theorem multichoose_zero_succ (k : ℕ) : multichoose (0 : R) (k + 1) = 0 := by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1)), factorial_nsmul_multichoose_eq_ascPochhammer, smul_zero,
    ascPochhammer_succ_left, smeval_X_mul, zero_mul]

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

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

Разделы

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

Аффилиация

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