Theorems · Theorem · combinatorics

Finset.sum_choose_succ_nsmul

∀ {M : Type u_2} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ),
  ∑ i ∈ Finset.range (n + 2), (n + 1).choose i • f i (n + 1 - i) =
    ∑ i ∈ Finset.range (n + 1), n.choose i • f i (n + 1 - i) +
      ∑ i ∈ Finset.range (n + 1), n.choose i • f (i + 1) (n - i)

Defined in

Mathlib.Data.Nat.Choose.Sum

Cited by

2 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoid