Commit 2020-04-13 14:53 f3ac7b70

View on Github ā†’

feat(combinatorics/composition): introduce compositions of an integer (#2398) A composition of an integer n is a decomposition of {0, ..., n-1} into blocks of consecutive integers. Equivalently, it is a decomposition n = iā‚€ + ... + i_{k-1} into a sum of positive integers. We define compositions in this PR, and introduce a whole interface around it. The goal is to use this as a tool in the proof that the composition of analytic functions is analytic

Estimated changes

added theorem composition.blocks_pos
added theorem composition.blocks_sum
added theorem composition.length_le
added structure composition
added structure composition_as_set
added theorem composition_card