### Abstract

This entry provides a basic library for number partitions, defines the two-argument partition function through its recurrence relation and relates this partition function to the cardinality of number partitions. The main proof shows that the recursively-defined partition function with arguments n and k equals the cardinality of number partitions of n with exactly k parts. The combinatorial proof follows the proof sketch of Theorem 2.4.1 in Mazur's textbook `Combinatorics: A Guided Tour`. This entry can serve as starting point for various more intrinsic properties about number partitions, the partition function and related recurrence relations.

### License

BSD License

### Topics

- Mathematics/Combinatorics

### Session Card_Number_Partitions

- Additions_to_Main
- Number_Partition
- Card_Number_Partitions

### Used by

- Combinatorial Enumeration Algorithms
- The Twelvefold Way
- Euler’s Partition Theorem

## Cite

×

Card_Number_Partitions-AFP

    @article{Card_Number_Partitions-AFP,
      author  = {Lukas Bulwahn},
      title   = {Cardinality of Number Partitions},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Card_Number_Partitions.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Jan 14, 2016 : Isabelle2015