catalan_eq_centralBinom_div
theorem catalan_eq_centralBinom_div : ∀ (n : ℕ), catalan n = n.centralBinom / (n + 1)
This theorem states that for all natural numbers `n`, the `n`-th Catalan number is equal to the `n`-th central binomial coefficient divided by `n + 1`. The Catalan numbers are defined recursively, with the `n + 1`-th Catalan number being the sum of the product of the `i`-th and `(n - i)`-th Catalan numbers for all `i` in the range from 0 to `n`. On the other hand, the `n`-th central binomial coefficient is defined as the number of ways to choose `n` items from a set of `2n` items.
More concisely: The `n`-th Catalan number equals the `n`-th central binomial coefficient divided by `n + 1`.
|
catalan_succ
theorem catalan_succ : ∀ (n : ℕ), catalan (n + 1) = Finset.univ.sum fun i => catalan ↑i * catalan (n - ↑i)
The theorem `catalan_succ` states that for any given natural number `n`, the `(n + 1)`th Catalan number is equal to the sum of the product of the `i`th Catalan number and the `(n - i)`th Catalan number, where `i` ranges over all elements in the universal finite set (`Finset.univ`). In mathematical notation, this is represented as `catalan (n + 1) = ∑ i in Finset.univ, catalan i * catalan (n - i)`.
More concisely: The `(n + 1)`th Catalan number is the sum of the products of the `i`th Catalan number and the `(n - i)`th Catalan number, for all `i` in the universal finite set. In mathematical notation, `catalan (n + 1) = ∑ i in Finset.univ, catalan i * catalan (n - i)`.
|