Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-04 10:57 14aa1f7b

View on Github →

feat(combinatorics/composition): refactor compositions, split a list wrt a composition (#2554) Refactor composition, replacing in its definition a list of positive integers with a list of integers which are positive. This avoids going back and forth all the time between nat and pnat. Also introduce the ability to split a list of length n with respect to a composition c of n, giving rise to a list of c.length sublists whose join is the original list.

Estimated changes

deleted def composition.blocks
modified theorem composition.blocks_length
deleted theorem composition.blocks_pos
deleted theorem composition.blocks_sum
modified def composition.length
added def composition.ones