Theorems · Definition · number theory

Nat.Partition.genFun

{R : Type u_1} → [CommSemiring R] → (ℕ → ℕ → R) → PowerSeries R

Generating function associated with character $f(i, c)$ for partition functions, where $i$ is a part of the partition, and $c$ is the count of that part in the partition. The character function is multiplied within one n.Partition, and summed among all n.Partition for a fixed n. This way, each n is assigned a value, which we use as the coefficients of the power series. See the module docstring of Combinatorics.Enumerative.Partition.GenFun for more details.

Defined in

Mathlib.Combinatorics.Enumerative.Partition.GenFun

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiring