multichoose_neg_of_lt

Mathlib.RingTheory.Binomial

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

← MathLib Explorer

English

If n < k, then multichoose (−n) k = 0. The negativity combined with a larger second index forces a zero value.

Русский

Если n < k, то multichoose(−n, k) = 0.

LaTeX

$$$ \forall n,k\in\mathbb{N},\ n

Lean4

@[simp]
theorem multichoose_neg_of_lt (n k : ℕ) (h : n < k) : multichoose (-n : ℤ) k = 0 := by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero k), factorial_nsmul_multichoose_eq_ascPochhammer,
    smeval_ascPochhammer_neg_of_lt h, smul_zero]

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

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

Разделы

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

Аффилиация

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