Theorems · Theorem · number theory

PowerSeries.WithPiTopology.hasSum_pow_pentagonal_sub_pentagonalSeries

∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R],
  HasSum (fun k => (-1) ^ k * (PowerSeries.X ^ pentagonal (-↑k) - PowerSeries.X ^ pentagonal (↑k + 1)))
    (PowerSeries.pentagonalSeries R)

PowerSeries.pentagonalSeries as an infinite sum over natural numbers. In this version, terms are ordered by strictly increasing exponent pentagonal k for k = 0, 1, -1, 2, -2, 3, ..., and every two terms are grouped together.

Defined in

Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Cited by

1 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingTopologicalSpace