choose_zero_succ — Mathlib

English

For any natural n, the binomial coefficient choose 0 (n+1) equals 0.

Русский

Для любого натурального n верно choose 0 (n+1) = 0.

LaTeX

$$$ \forall n\in\mathbb{N},\ choose\ 0\ (n+1) = 0 $$$

Lean4

@[simp]
theorem choose_zero_succ (R) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R] (n : ℕ) :
    choose (0 : R) (n + 1) = 0 := by
  rw [choose, Nat.cast_succ, zero_sub, neg_add, neg_add_cancel_right, multichoose_succ_neg_natCast]

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