# Partitions #

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
of `n`

the order does matter.
A summand of the partition is called a part.

## Main functions #

`p : Partition n`

is a structure, made of a multiset of integers which are all positive and add up to`n`

.

## 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.

## Tags #

Partition

## References #

positive integers summing to

`n`

proof that the

`parts`

are positive- parts_sum : Multiset.sum s.parts = n
proof that the

`parts`

sum to`n`

A partition of `n`

is a multiset of positive integers summing to `n`

.

## Instances For

A composition induces a partition (just convert the list to a multiset).

## Instances For

Given a multiset which sums to `n`

, construct a partition of `n`

with the same multiset, but
without the zeros.

## Instances For

A `Multiset ℕ`

induces a partition on its sum.

## Instances For

The partition of exactly one part.

## Instances For

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 `l`

.
(For `i = 0`

, `Partition.non_zero`

combined with `Multiset.count_eq_zero_of_not_mem`

gives that
this is `0`

instead.)

Show there are finitely many partitions by considering the surjection from compositions to partitions.

The finset of those partitions in which every part is odd.

## Instances For

The finset of those partitions in which each part is used at most once.

## Instances For

The finset of those partitions in which every part is odd and used at most once.