Commit 2026-02-13 04:22 35fe6a06

View on Github →

chore: make Dyck word definitions public (#34143)

equivTreeToFun -> toTree
equivTreeInvFun -> ofTree Also remove the two unusedHavesSuffices nolints from a time when the linter was not as discerning.

Estimated changes

Modified Mathlib/Combinatorics/Enumerative/DyckWord.lean

modified def DyckWord.equivTree

modified def DyckWord.equivTreesOfNumNodesEq

added theorem DyckWord.numNodes_toTree

added def DyckWord.ofTree

added theorem DyckWord.ofTree_toTree

deleted theorem DyckWord.semilength_eq_numNodes_equivTree

added def DyckWord.toTree

added theorem DyckWord.toTree_ofTree