Theorems · Theorem · combinatorics

Finset.prod_pow_choose_succ

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

Defined in

Mathlib.Data.Nat.Choose.Sum

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoid