Theorems · Theorem · commutative algebra

MvPolynomial.coeff_add_pow

∀ {R : Type u_1} [inst : CommSemiring R] (d : Fin 2 →₀ ℕ) (n : ℕ),
  MvPolynomial.coeff d ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ n) =
    ↑(if (d 0, d 1) ∈ Finset.HasAntidiagonal.antidiagonal n then n.choose (d 0) else 0)

The formula for the dth coefficient of (X 0 + X 1) ^ n.

Defined in

Mathlib.Algebra.MvPolynomial.Coeff

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiring