Documentation

Mathlib.Combinatorics.Partition

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 #

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.

TODO #

Link this to Young diagrams.

Tags #

Partition

References #

theorem Nat.Partition.ext {n : } (x : Nat.Partition n) (y : Nat.Partition n) (parts : x.parts = y.parts) :
x = y
theorem Nat.Partition.ext_iff {n : } (x : Nat.Partition n) (y : Nat.Partition n) :
x = y x.parts = y.parts
structure Nat.Partition (n : ) :

A partition of n is a multiset of positive integers summing to n.

Instances For
    Equations
    @[simp]
    theorem Nat.Partition.ofComposition_parts (n : ) (c : Composition n) :
    (Nat.Partition.ofComposition n c).parts = c.blocks

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

    Equations
    Instances For
      @[simp]
      theorem Nat.Partition.ofSums_parts (n : ) (l : Multiset ) (hl : Multiset.sum l = n) :
      (Nat.Partition.ofSums n l hl).parts = Multiset.filter (fun (x : ) => x 0) l

      Given a multiset which sums to n, construct a partition of n with the same multiset, but without the zeros.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The partition of exactly one part.

        Equations
        Instances For
          Equations
          @[simp]
          theorem Nat.Partition.indiscrete_parts {n : } (hn : n 0) :
          @[simp]
          Equations
          @[simp]
          Equations
          theorem Nat.Partition.count_ofSums_of_ne_zero {n : } {l : Multiset } (hl : Multiset.sum l = n) {i : } (hi : i 0) :

          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.

          Equations

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

          Equations
          Instances For

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

            Equations
            Instances For

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

              Equations
              Instances For