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
Imports
Idea
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
- 2023-03-21. Fredrik Bakke. Formatting fixes (#530).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).
- 2023-02-13. Jonathan Prieto-Cubides. Nueva era (#445).
- 2023-02-05. Fredrik Bakke. remove redundant pragmas.