Commit 2025-03-24 10:45 8412ecb7

View on Github →

chore(Combinatorics/Composition): add missing API lemmas (#22430) Also define Composition.cast, Composition.append, Composition.reverse, as well as 2 recursion principles.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/List/Basic.lean

modified theorem List.prod_reverse

Modified Mathlib/Combinatorics/Enumerative/Composition.lean

added def Composition.append

added theorem Composition.blocks_eq_nil

added theorem Composition.blocks_le

added theorem Composition.cast_eq_cast

added theorem Composition.cast_heq

added theorem Composition.cast_rfl

added theorem Composition.length_pos_iff

deleted theorem Composition.length_pos_of_pos

added def Composition.recOnAppendSingle

added def Composition.recOnSingleAppend

added def Composition.reverse

added theorem Composition.reverse_append

added theorem Composition.reverse_bijective

added theorem Composition.reverse_eq_ones

added theorem Composition.reverse_eq_single

added theorem Composition.reverse_inj

added theorem Composition.reverse_injective

added theorem Composition.reverse_involutive

added theorem Composition.reverse_ones

added theorem Composition.reverse_reverse

added theorem Composition.reverse_single

added theorem Composition.reverse_surjective