d'Ocagne's identity for the Vieta–Fibonacci polynomials

Mathlib's Polynomial.Chebyshev.S are the rescaled Chebyshev polynomials of the second kind (Vieta–Fibonacci polynomials), indexed by ℤ, with the Cassini-type identity S_sq_add_S_sq. This file proves the two-index identity of which that is the case q = p + 1:

S p * S (q - 1) - S q * S (p - 1) = - S (p - q - 1).

Main results

• Orbit.S_docagne: d'Ocagne's identity.
• Orbit.S_sq_add_S_sq_of_docagne: Mathlib's S_sq_add_S_sq recovered from it.

theorem Orbit.S_docagne (R : Type u_1) [CommRing R] (p q : ℤ) : Polynomial.Chebyshev.S R p * Polynomial.Chebyshev.S R (q - 1) - Polynomial.Chebyshev.S R q * Polynomial.Chebyshev.S R (p - 1) = -Polynomial.Chebyshev.S R (p - q - 1)

d'Ocagne's identity for the Vieta–Fibonacci polynomials S. Classical.

theorem Orbit.S_sq_add_S_sq_of_docagne (R : Type u_1) [CommRing R] (n : ℤ) : Polynomial.Chebyshev.S R n ^ 2 + Polynomial.Chebyshev.S R (n + 1) ^ 2 - Polynomial.X * Polynomial.Chebyshev.S R n * Polynomial.Chebyshev.S R (n + 1) = 1

Mathlib's S_sq_add_S_sq is the case q = p + 1, recovered as a consistency check.