mathlib documentation


Catalan numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_central_binom_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)

theorem catalan_zero  :
theorem catalan_succ (n : ) :
catalan (n + 1) = finset.univ.sum (λ (i : fin n.succ), catalan i * catalan (n - i))
theorem catalan_succ' (n : ) :
theorem catalan_one  :
theorem catalan_two  :
theorem catalan_three  :

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

@[simp, norm_cast]