Theorems · Definition · combinatorics
catalan
ℕ → ℕ
The recursive definition of the sequence of Catalan numbers:
catalan (n + 1) = ∑ i : Fin n.succ, catalan i * catalan (n - i)
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finset.sumproof · cited by 5,195
- Finset.univproof · cited by 3,473
Cited by14
Results whose statement or proof uses this declaration.
- catalan_zerostatement · cited by 5
- PowerSeries.catalanSeriesproof · cited by 3
- catalan_eq_centralBinom_divstatement and proof · cited by 3
- catalan_succstatement and proof · cited by 3
- PowerSeries.catalanSeries_coeffstatement and proof · cited by 2
- catalan_succ'statement and proof · cited by 2
- BinaryTree.treesOfNumNodesEq_card_eq_catalanstatement and proof · cited by 1
- catalan.eq_defstatement and proof · cited by 0
- succ_mul_catalan_eq_centralBinomstatement · cited by 0
- PowerSeries.catalanSeries_sq_mul_X_add_oneproof · cited by 0
- DyckWord.card_dyckWord_semilength_eq_catalanstatement and proof · cited by 0
- catalan_onestatement and proof · cited by 0