[isabelle] new in the AFP: Cardinality of Number Partitions

The first AFP entry for 2016 is now online:


 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.

Many thanks to Lukas Bulwahn for this contribution!


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.