multichoose_neg_succ — Mathlib

English

For any natural n, multichoose (−n) (n+1) equals 0. This is a vanishing property of the multichoose polynomial at consecutive indices with negative first argument.

Русский

Для любого натурального n имеет значение multichoose(−n, n+1) = 0.

LaTeX

$$$ \forall n\in\mathbb{N},\quad \operatorname{multichoose}( -n\,\mathbb{Z},\, n+1) = 0 $$$

Lean4

@[simp]
theorem multichoose_neg_succ (n : ℕ) : multichoose (-n : ℤ) (n + 1) = 0 := by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero _), factorial_nsmul_multichoose_eq_ascPochhammer,
    smeval_ascPochhammer_succ_neg, smul_zero]

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