Assumptions:
TeX:
F_{n} = \sum_{k=0}^{n - 1} {n - k - 1 \choose k} n \in \mathbb{Z}_{\ge 0}
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
Fibonacci | Fibonacci number | |
Sum | Sum | |
Binomial | Binomial coefficient | |
ZZGreaterEqual | Integers greater than or equal to n |
Source code for this entry:
Entry(ID("9638c1"), Formula(Equal(Fibonacci(n), Sum(Binomial(Sub(Sub(n, k), 1), k), For(k, 0, Sub(n, 1))))), Variables(n), Assumptions(Element(n, ZZGreaterEqual(0))))