Theorems · Theorem · combinatorics

Finset.prod_antidiagonal_pow_choose_succ

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

Defined in

Mathlib.Data.Nat.Choose.Sum

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoid