multichoose_succ_neg_natCast — Mathlib

English

For any natural n, multichoose (−n) (n+1) equals 0 when interpreted in a ring with NatPowAssoc structure. This mirrors the NatCast case for succ.

Русский

Для любого натурального n, multichoose(−n) (n+1) = 0 в кольце с NatPowAssoc.

LaTeX

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

Lean4

theorem multichoose_succ_neg_natCast [NatPowAssoc R] (n : ℕ) : multichoose (-n : R) (n + 1) = 0 := by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + 1)), smul_zero, factorial_nsmul_multichoose_eq_ascPochhammer,
    smeval_neg_nat, smeval_ascPochhammer_succ_neg n, Int.cast_zero]

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