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.
Given a multiset which sums to
n, construct a partition of
n with the same multiset, but
without the zeros.
The number of times a positive integer
i appears in the partition
of_sums 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
Show there are finitely many partitions by considering the surjection from compositions to partitions.