The lowest coefficient of a product of power series without constant term

A power series with vanishing constant coefficient is a multiple of X, so a product of n such series is a multiple of X ^ n, and its coefficient in degree n is the product of the linear coefficients of the factors. This file records that computation, with an extra factor g in front whose constant coefficient comes along:

coeff |s| (g * ∏_{i ∈ s} f i) = g(0) * ∏_{i ∈ s} f i'(0)

whenever every f i has zero constant coefficient. It is the "leading term" extraction behind limit arguments such as the Weyl dimension formula, where a product of |Φ⁺| factors each of order one is divided by another such product.

Main results

• PowerSeries.coeff_card_mul_prod_of_constantCoeff_eq_zero: the coefficient of g * ∏_{i ∈ s} f i in degree |s| is constantCoeff g * ∏_{i ∈ s} coeff 1 (f i) when each f i has zero constant coefficient.

theorem PowerSeries.coeff_card_mul_prod_of_constantCoeff_eq_zero {R : Type u_1} [CommSemiring R] {ι : Type u_2} (s : Finset ι) {f : ι → PowerSeries R} (hf : ∀ i ∈ s, constantCoeff (f i) = 0) (g : PowerSeries R) : (coeff s.card) (g * ∏ i ∈ s, f i) = constantCoeff g * ∏ i ∈ s, (coeff 1) (f i)

The lowest coefficient of a product of power series without constant term. If each f i, i ∈ s, has zero constant coefficient, then g * ∏_{i ∈ s} f i has order at least |s|, and its coefficient in degree |s| is the constant coefficient of g times the product of the linear coefficients of the f i.