FPS Euler Second Identity

We prove the Euler second identity purely algebraically in the formal power series ring: qPochhammerInf(-a) = Σ_{n≥0} X^{C(n,2)} · aⁿ · (qPochhammer(X, n))⁻¹

The proof uses the finite q-binomial theorem (which holds in any commutative ring) and takes the limit in the pi topology. The key step is showing that the Gaussian binomial coefficient qBinom(N, k, X) converges to (qPochhammer(X, k))⁻¹ as N → ∞.

theorem QSeries.FormalPowerSeries.constantCoeff_qPochhammer_X {R : Type u_1} [CommRing R] (n : ℕ) : PowerSeries.constantCoeff (qPochhammer PowerSeries.X n) = 1

The constant term of qPochhammer X n is 1.

theorem QSeries.FormalPowerSeries.isUnit_qPochhammer_X {R : Type u_1} [CommRing R] (n : ℕ) : IsUnit (qPochhammer PowerSeries.X n)

qPochhammer X n is a unit in R⟦X⟧ (its constant term is 1).

theorem QSeries.FormalPowerSeries.qPochhammerInf_eq_qPochhammer_mul {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (a : PowerSeries R) (n : ℕ) : qPochhammerInf a = qPochhammer a n * qPochhammerInf (a * PowerSeries.X ^ n)

qPochhammerInf a = qPochhammer a n · qPochhammerInf (a · X^n).

theorem QSeries.FormalPowerSeries.qPochhammerInf_X_eq_qPochhammer_mul {R : Type u_1} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (n : ℕ) : qPochhammerInf PowerSeries.X = qPochhammer PowerSeries.X n * qPochhammerInf (PowerSeries.X * PowerSeries.X ^ n)

qPochhammerInf X = qPochhammer X n · qPochhammerInf (X * X^n).