Commit 2022-06-26 17:01 54352be4

feat(combinatorics/catalan): definition and equality of recursive and explicit definition (#14869) This PR defines the Catalan numbers via the recursive definition $$C (n+1) = \sum_{i=0}^n C (i) * C (n-i)$$. Furthermore, it shows that $$ n+1 | \binom {2n}{n}$$ and that the alternative $$C(n)=\frac{1}{n+1} \binom{2n}{n}$$ holds. The proof is based on the following stackexchange answer: https://math.stackexchange.com/questions/3304415/catalan-numbers-algebraic-proof-of-the-recurrence-relation which is quite elementary, so that the proof is relatively easy to formalise.