mathlib3

f3ac7b70 - feat(combinatorics/composition): introduce compositions of an integer (#2398)

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