Polynomial products as power series

MvPolynomial.coe_finsuppProd_pow moves a finitely supported product of polynomial powers through the coercion to multivariate power series. It lets coefficient computations for such products use the polynomial API, for example when substituting polynomials into power series. The coefficient semiring need only be commutative; no norm or topology is required.

MvPowerSeries.coeff_X_add_X_pow is the binomial formula for the coefficients of (X + Y) ^ n in R⟦X, Y⟧, the power-series counterpart of MvPolynomial.coeff_add_pow, over any semiring.

@[simp]

theorem MvPolynomial.coe_finsuppProd_pow {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (a : σ → MvPolynomial τ R) (d : σ →₀ ℕ) : ↑(d.prod fun (s : σ) (n : ℕ) => a s ^ n) = d.prod fun (s : σ) (n : ℕ) => ↑(a s) ^ n

The coercion of polynomials to power series commutes with products of powers.

theorem MvPowerSeries.coeff_X_add_X_pow {R : Type u_1} [Semiring R] (d : Fin 2 →₀ ℕ) (n : ℕ) : (coeff d) ((X 0 + X 1) ^ n) = if d 0 + d 1 = n then ↑(n.choose (d 0)) else 0

The coefficient of X^(d 0) Y^(d 1) in (X + Y) ^ n is n.choose (d 0) if d 0 + d 1 = n, and 0 otherwise.