Mathlib v3 is deprecated. Go to Mathlib v4

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
added theorem fin.coe_last
modified theorem fin.coe_mk
deleted theorem finset.bij_on_mono_of_fin
added theorem list.of_fn_prod
added theorem list.of_fn_prod_take
added theorem list.of_fn_sum_take
added theorem list.eq_of_sum_take_eq
added theorem list.monotone_sum_take
added theorem list.map_of_fn
added theorem list.nth_le_of_fn'
modified theorem list.nth_le_of_fn