Theorems · Theorem · number theory

PowerSeries.coeff_prod_one_sub_X_pow_eventually_eq

∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  ∀ᶠ (s : Finset ℕ) in Filter.atTop,
    (PowerSeries.coeff n) (∏ n ∈ s, (1 - PowerSeries.X ^ (n + 1))) =
      (PowerSeries.coeff n) (PowerSeries.pentagonalSeries R)

Pentagonal number theorem for power series, expressed as the statement that the coefficients of the product ∏ n, 1 - X ^ (n + 1) are eventually constants as (pentagonalSeries R).coeff.

Defined in

Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing