Zulip Chat Archive

Are there any results for partition numbers (i.e. number of partitions)? There exists combinatorics/partition.leanbut it only defines a partition as a multiset that sums to a number, but not the number of partitions. There's also this interesting comment

## Implementation details

The main motivation for this structure and its API is to show Euler's partition theorem, and
related results.

The representation of a partition as a multiset is very handy as multisets are very flexible and
already have a well-developed API

But I can't find any mention of Euler's partition theorem / pentagonal theorem

Yaël Dillies (Jan 28 2023 at 07:43):

cc @Bhavik Mehta

Gareth Ma (Jan 29 2023 at 00:49):

What if I want to define it myself? How should I approach it to get a definition that I can actually prove results on

Gareth Ma (Jan 29 2023 at 00:50):

For us humans it’s natural to jump directly to generating function and the infinite product prod(1/(1-x^p))

Gareth Ma (Jan 29 2023 at 00:51):

But i don’t know if it’s possible to translate this to lean? If anyone can provide some directions that would be nice

Gareth Ma (Jan 29 2023 at 00:52):

Like preferably the definition would somehow be “counting number of distinct partitions” instead of an arbitrary function defined as the coefficient of the product