multichoose_neg_self — Mathlib

English

For every natural n, multichoose (−n) n equals (−1)^n. This shows a parity-like behavior for the multichoose polynomial evaluated at a negative integer argument paired with its positive index.

Русский

Для каждого натурального n выполняется равенство multichoose(−n, n) = (−1)^n, то есть поведение по знаку аналогично знаку паритета.

LaTeX

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

Lean4

theorem multichoose_neg_self (n : ℕ) : multichoose (-n : ℤ) n = (-1) ^ n := by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero _), factorial_nsmul_multichoose_eq_ascPochhammer,
    smeval_ascPochhammer_self_neg, nsmul_eq_mul, Nat.cast_comm]

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