Commit 2023-02-13 21:20 3e322ac2

View on Github →

feat: Port/Combinatorics.Composition (#2043)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Composition.lean

added def Composition.blocksFinEquiv

added def Composition.blocksFun

added theorem Composition.blocksFun_congr

added theorem Composition.blocksFun_mem_blocks

added theorem Composition.blocks_length

added theorem Composition.blocks_pos'

added def Composition.boundaries

added def Composition.boundary

added theorem Composition.boundary_last

added theorem Composition.boundary_zero

added theorem Composition.card_boundaries_eq_succ_length

added theorem Composition.coe_embedding

added theorem Composition.coe_invEmbedding

added theorem Composition.disjoint_range

added def Composition.embedding

added theorem Composition.embedding_comp_inv

added theorem Composition.eq_ones_iff

added theorem Composition.eq_ones_iff_le_length

added theorem Composition.eq_ones_iff_length

added theorem Composition.eq_single_iff_length

added def Composition.index

added theorem Composition.index_embedding

added theorem Composition.index_exists

added def Composition.invEmbedding

added theorem Composition.invEmbedding_comp

added def Composition.length

added theorem Composition.length_le

added theorem Composition.length_pos_of_pos

added theorem Composition.lt_sizeUpTo_index_succ

added theorem Composition.mem_range_embedding

added theorem Composition.mem_range_embedding_iff'

added theorem Composition.mem_range_embedding_iff

added theorem Composition.monotone_sizeUpTo

added theorem Composition.ne_ones_iff

added theorem Composition.ne_single_iff

added theorem Composition.ofFn_blocksFun

added theorem Composition.one_le_blocks'

added theorem Composition.one_le_blocks

added theorem Composition.one_le_blocksFun

added def Composition.ones

added theorem Composition.ones_blocks

added theorem Composition.ones_blocksFun

added theorem Composition.ones_embedding

added theorem Composition.ones_length

added theorem Composition.ones_sizeUpTo

added theorem Composition.orderEmbOfFin_boundaries

added theorem Composition.sigma_eq_iff_blocks_eq

added def Composition.single

added theorem Composition.single_blocks

added theorem Composition.single_blocksFun

added theorem Composition.single_embedding

added theorem Composition.single_length

added def Composition.sizeUpTo

added theorem Composition.sizeUpTo_index_le

added theorem Composition.sizeUpTo_le

added theorem Composition.sizeUpTo_length

added theorem Composition.sizeUpTo_ofLength_le

added theorem Composition.sizeUpTo_strict_mono

added theorem Composition.sizeUpTo_succ'

added theorem Composition.sizeUpTo_succ

added theorem Composition.sizeUpTo_zero

added theorem Composition.sum_blocksFun

added def Composition.toCompositionAsSet

added theorem Composition.toCompositionAsSet_blocks

added theorem Composition.toCompositionAsSet_boundaries

added theorem Composition.toCompositionAsSet_length

added structure Composition

added def CompositionAsSet.blocks

added def CompositionAsSet.blocksFun

added theorem CompositionAsSet.blocksFun_pos

added theorem CompositionAsSet.blocks_length

added theorem CompositionAsSet.blocks_partial_sum

added theorem CompositionAsSet.blocks_sum

added theorem CompositionAsSet.boundaries_nonempty

added def CompositionAsSet.boundary

added theorem CompositionAsSet.boundary_length

added theorem CompositionAsSet.boundary_zero

added theorem CompositionAsSet.card_boundaries_eq_succ_length

added theorem CompositionAsSet.card_boundaries_pos

added def CompositionAsSet.length

added theorem CompositionAsSet.length_lt_card_boundaries

added theorem CompositionAsSet.lt_length'

added theorem CompositionAsSet.lt_length

added theorem CompositionAsSet.mem_boundaries_iff_exists_blocks_sum_take_eq

added def CompositionAsSet.toComposition

added theorem CompositionAsSet.toComposition_blocks

added theorem CompositionAsSet.toComposition_boundaries

added theorem CompositionAsSet.toComposition_length

added structure CompositionAsSet

added theorem List.join_splitWrtComposition

added theorem List.join_splitWrtCompositionAux

added theorem List.length_pos_of_mem_splitWrtComposition

added theorem List.length_splitWrtComposition

added theorem List.length_splitWrtCompositionAux

added theorem List.map_length_splitWrtComposition

added theorem List.map_length_splitWrtCompositionAux

added theorem List.nthLe_splitWrtComposition

added theorem List.nthLe_splitWrtCompositionAux

added def List.splitWrtComposition

added def List.splitWrtCompositionAux

added theorem List.splitWrtCompositionAux_cons

added theorem List.splitWrtComposition_join

added theorem List.sum_take_map_length_splitWrtComposition

added def compositionAsSetEquiv

added theorem compositionAsSet_card

added def compositionEquiv

added theorem composition_card