multichoose_neg_add — Mathlib

English

For natural n and k, multichoose (−n) (n + k + 1) equals 0. This extends the vanishing property to a family with additive shift.

Русский

Для любых n,k ∈ ℕ выполняется multichoose(−n, n+k+1) = 0.

LaTeX

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

Lean4

theorem multichoose_neg_add (n k : ℕ) : multichoose (-n : ℤ) (n + k + 1) = 0 := by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + k + 1)), factorial_nsmul_multichoose_eq_ascPochhammer,
    smeval_ascPochhammer_neg_add, smul_zero]

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