Theorems · Theorem · number theory

Nat.Partition.hasProd_powerSeriesMk_card_restricted

∀ (R : Type u_1) [inst : TopologicalSpace R] [T2Space R] [inst_2 : CommSemiring R] [IsTopologicalSemiring R]
  (p : ℕ → Prop) [inst_4 : DecidablePred p],
  HasProd (fun i => if p (i + 1) then ∑' (j : ℕ), PowerSeries.X ^ ((i + 1) * j) else 1)
    (PowerSeries.mk fun n => ↑(Nat.Partition.restricted n p).card)

The generating function of Nat.Partition.restricted n p is $$ \prod_{i \in p} \sum_{j = 0}^{\infty} X^{ij} $$

Defined in

Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceT2SpaceCommSemiringIsTopologicalSemiringDecidablePred