[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