Formulas for coefficients of multivariate polynomials

Main Results

• MvPolynomial.coeff_add_pow: the formula for the dth coefficient of (X 0 + X 1) ^ n.

theorem MvPolynomial.coeff_linearCombination_X_pow {R : Type u_1} {σ : Type u_2} [CommSemiring R] (a : σ →₀ R) (s : σ →₀ ℕ) (n : ℕ) : coeff s ((Finsupp.linearCombination R X) a ^ n) = if (s.sum fun (x : σ) (m : ℕ) => m) = n then ↑s.multinomial * s.prod fun (r : σ) (m : ℕ) => a r ^ m else 0

theorem MvPolynomial.coeff_linearCombination_X_pow_of_fintype {R : Type u_1} {σ : Type u_2} [CommSemiring R] [Fintype σ] (a : σ → R) (s : σ →₀ ℕ) (n : ℕ) : coeff s ((∑ i : σ, a i • X i) ^ n) = if (s.sum fun (x : σ) (m : ℕ) => m) = n then ↑s.multinomial * s.prod fun (r : σ) (m : ℕ) => a r ^ m else 0

theorem MvPolynomial.coeff_sum_X_pow_of_fintype {R : Type u_1} {σ : Type u_2} [CommSemiring R] [Fintype σ] (d : σ →₀ ℕ) (n : ℕ) : coeff d ((∑ i : σ, X i) ^ n) = ↑(if (d.sum fun (x : σ) (m : ℕ) => m) = n then d.multinomial else 0)

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

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

theorem MvPolynomial.monomial_fin_two {R : Type u_1} [CommSemiring R] (d : Fin 2 →₀ ℕ) (a : R) : (monomial d) a = C a * X 0 ^ d 0 * X 1 ^ d 1

A monomial in two variables equals C a * X 0 ^ d 0 * X 1 ^ d 1.