Integer partitions

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-04-25.
Last modified on 2023-03-21.

module elementary-number-theory.integer-partitions where


An integer partition of a natural number n is a list of nonzero natural numbers that sum up to n, up to reordering. We define the number p n of integer partitions of n as the number of connected components in the type of finite Ferrer diagrams of Fin n.

Recent changes