# Cardinality of Number Partitions

 Title: Cardinality of Number Partitions Author: Lukas Bulwahn (lukas /dot/ bulwahn /at/ gmail /dot/ com) Submission date: 2016-01-14 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. BibTeX: @article{Card_Number_Partitions-AFP, author = {Lukas Bulwahn}, title = {Cardinality of Number Partitions}, journal = {Archive of Formal Proofs}, month = jan, year = 2016, note = {\url{http://isa-afp.org/entries/Card_Number_Partitions.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: Euler_Partition, Twelvefold_Way