A partition of a natural number
n is a way of writing
n as a sum of positive integers, where the
order does not matter: two sums that differ only in the order of their summands are considered the
same partition. This notion is closely related to that of a composition of
n, but in a composition
n the order does matter.
A summand of the partition is called a part.
Main functions #
p : Partition nis a structure, made of a multiset of integers which are all positive and add up to
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.
A partition of
n is a multiset of positive integers summing to
The number of times a positive integer
i appears in the partition
ofSums n l hl is the same
as the number of times it appears in the multiset
i = 0,
Partition.non_zero combined with
Multiset.count_eq_zero_of_not_mem gives that