Commit 2023-02-08 14:04 26b40791

View on Github →

feat(combinatorics/catalan): Connection between Catalan numbers and number of trees (#16583) Shows that the number of binary trees with n nodes is the nth Catalan number.

Estimated changes

Modified src/combinatorics/catalan.lean

added theorem catalan_succ'

added theorem tree.coe_trees_of_nodes_eq

added theorem tree.mem_trees_of_nodes_eq

added theorem tree.mem_trees_of_nodes_eq_num_nodes

added def tree.pairwise_node

added theorem tree.trees_of_nodes_eq_card_eq_catalan

added theorem tree.trees_of_nodes_eq_succ

added theorem tree.trees_of_nodes_eq_zero

added def tree.trees_of_num_nodes_eq