Commit 2024-08-16 05:39 76ccc39d

View on Github →

feat: Dyck words up to semilength (#14162) First part of #9781.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Enumerative/DyckWord.lean

added theorem DyckStep.dichotomy

added inductive DyckStep

added theorem DyckWord.cons_tail_dropLast_concat

added def DyckWord.denest

added theorem DyckWord.denest_nest

added def DyckWord.drop

added theorem DyckWord.getLast_eq_D

added theorem DyckWord.head_eq_U

added def DyckWord.nest

added def DyckWord.semilength

added theorem DyckWord.semilength_add

added theorem DyckWord.semilength_eq_count_D

added theorem DyckWord.semilength_nest

added theorem DyckWord.semilength_zero

added def DyckWord.take

added theorem DyckWord.toList_eq_nil

added theorem DyckWord.two_mul_semilength_eq_length

added structure DyckWord