Infinite products of power series in the coefficientwise topology

If all but finitely many factors agree with 1 to each prescribed degree, their product converges coefficientwise. Each coefficient is computed from any finite cutoff containing all factors that can affect it.

Main results

• PowerSeries.WithPiTopology.hasProd_of_X_pow_dvd_sub_one: convergence and finite-cutoff coefficients for products whose factors approach 1 modulo increasing powers of X.

theorem PowerSeries.WithPiTopology.hasProd_of_X_pow_dvd_sub_one {R : Type u_1} {ι : Type u_2} [CommRing R] [TopologicalSpace R] {g : ι → PowerSeries R} (F : ℕ → Finset ι) (hF : ∀ (n : ℕ), ∀ i ∉ F n, X ^ (n + 1) ∣ g i - 1) : HasProd g (mk fun (n : ℕ) => (coeff n) (∏ i ∈ F n, g i))

Infinite products through finite cutoffs. If, for each n, every factor g i with i ∉ F n is congruent to 1 modulo X ^ (n + 1), then the product of all the g i converges in the coefficientwise topology, and its n-th coefficient is that of ∏ i ∈ F n, g i.