mathlib3

54352be4 - feat(combinatorics/catalan): definition and equality of recursive and explicit definition (#14869)

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. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>