Catalan numbers #
The Catalan numbers (http://oeis.org/A000108) are probably the most ubiquitous sequence of integers in mathematics. They enumerate several important objects like binary trees, Dyck paths, and triangulations of convex polygons.
Main definitions #
catalan n: the
nth Catalan number, defined recursively as
catalan (n + 1) = ∑ i : Fin n.succ, catalan i * catalan (n - i).
Main results #
treesOfNodesEq_card_eq_catalan: The number of binary trees with
ninternal nodes is
Implementation details #
The proof of
catalan_eq_centralBinom_div follows https://math.stackexchange.com/questions/3304415
- Prove that the Catalan numbers enumerate many interesting objects.
- Provide the many variants of Catalan numbers, e.g. associated to complex reflection groups, Fuss-Catalan, etc.