Commit 2026-04-29 10:38 ccfee270

View on Github →

chore(Combinatorics/Enumerative/Catalan): split into Basic & Tree (#34854)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/Enumerative/Catalan.lean

deleted theorem Tree.coe_treesOfNumNodesEq

deleted theorem Tree.mem_treesOfNumNodesEq

deleted theorem Tree.mem_treesOfNumNodesEq_numNodes

deleted def Tree.treesOfNumNodesEq

deleted theorem Tree.treesOfNumNodesEq_card_eq_catalan

deleted theorem Tree.treesOfNumNodesEq_succ

deleted theorem Tree.treesOfNumNodesEq_zero

deleted def catalan

deleted theorem catalan_eq_centralBinom_div

deleted theorem catalan_one

deleted theorem catalan_succ'

deleted theorem catalan_succ

deleted theorem catalan_three

deleted theorem catalan_two

deleted theorem catalan_zero

deleted theorem succ_mul_catalan_eq_centralBinom

Created Mathlib/Combinatorics/Enumerative/Catalan/Basic.lean

added def catalan

added theorem catalan_eq_centralBinom_div

added theorem catalan_one

added theorem catalan_succ'

added theorem catalan_succ

added theorem catalan_three

added theorem catalan_two

added theorem catalan_zero

added theorem succ_mul_catalan_eq_centralBinom

Created Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean

added theorem Tree.coe_treesOfNumNodesEq

added theorem Tree.mem_treesOfNumNodesEq

added theorem Tree.mem_treesOfNumNodesEq_numNodes

added def Tree.treesOfNumNodesEq

added theorem Tree.treesOfNumNodesEq_card_eq_catalan

added theorem Tree.treesOfNumNodesEq_succ

added theorem Tree.treesOfNumNodesEq_zero

Modified Mathlib/Combinatorics/Enumerative/DyckWord.lean

Modified Mathlib/RingTheory/PowerSeries/Catalan.lean