Catalan's identity
Assumptions:
TeX:
F_{n}^{2} = F_{n + m} F_{n - m} + {\left(-1\right)}^{n + m} F_{m}^{2}
n \in \mathbb{Z} \;\mathbin{\operatorname{and}}\; m \in \mathbb{Z}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| Pow | Power | |
| Fibonacci | Fibonacci number | |
| ZZ | Integers |
Source code for this entry:
Entry(ID("ab563e"),
Formula(Equal(Pow(Fibonacci(n), 2), Add(Mul(Fibonacci(Add(n, m)), Fibonacci(Sub(n, m))), Mul(Pow(-1, Add(n, m)), Pow(Fibonacci(m), 2))))),
Description("Catalan's identity"),
Variables(n, m),
Assumptions(And(Element(n, ZZ), Element(m, ZZ))))