Generalize the partial-product convergence converse

[faabian]

Summary

• prove that coefficientwise convergence of initial partial products implies PowerSeries.Multipliable in the general finitely-determined sense
• prove that the resulting general infinite product equals the coefficientwise limit
• remove the constant-coefficient-one restriction from the blueprint mapping for thm.fps.lim.prod-lim-conv

Proof idea

For coefficient degree n, choose an initial segment after which every partial product is x^n-equivalent to the limit. Comparing the partial products immediately before and after any later factor shows that this initial product absorbs that factor modulo x^(n+1). Induction over an arbitrary finite set of later factors then proves that the initial segment determines coefficient n. This works over an arbitrary commutative ring and does not require cancellation, units, or normalized constant coefficients.

Validation

• lake build AlgebraicCombinatorics.FPS.InfiniteProducts
• lake build (8,078 jobs; succeeds)
• #print axioms for both new public theorems reports only propext, Classical.choice, and Quot.sound

The pre-existing project-wide sorry warnings in unrelated LGV, Jacobi–Trudi, and Desnanot–Jacobi declarations are unchanged.