Catalan numbers #

The Catalan numbers ( 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 #

Main results #

Implementation details #

The proof of catalan_eq_centralBinom_div follows


def catalan :

The recursive definition of the sequence of Catalan numbers: catalan (n + 1) = ∑ i : Fin n.succ, catalan i * catalan (n - i)

Instances For
    theorem catalan_zero :
    theorem catalan_succ (n : ) :
    catalan (n + 1) = Finset.sum Finset.univ fun i => catalan i * catalan (n - i)
    theorem catalan_succ' (n : ) :
    catalan (n + 1) = Finset.sum (Finset.Nat.antidiagonal n) fun ij => catalan ij.fst * catalan ij.snd
    theorem catalan_one :

    Given two finsets, find all trees that can be formed with left child in a and right child in b

    Instances For

      A Finset of all trees with n nodes. See mem_treesOfNodesEq

      Instances For