Commit 2023-03-13 14:02 dec364a4

View on Github →

feat: Port Combinatorics.Catalan (#2588)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Catalan.lean

added theorem Tree.coe_treesOfNodesEq

added theorem Tree.mem_treesOfNodesEq

added theorem Tree.mem_trees_of_nodes_eq_numNodes

added def Tree.pairwiseNode

added theorem Tree.treesOfNodesEq_card_eq_catalan

added theorem Tree.treesOfNodesEq_succ

added theorem Tree.treesOfNodesEq_zero

added def Tree.treesOfNumNodesEq

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