English
Let R be a commutative ring. For all integers m and k, C_R(m) C_R(k) = C_R(m+k) + C_R(m-k).
Русский
Пусть R — коммутативное кольцо. Для любых целых m и k выполняется равенство C_R(m) C_R(k) = C_R(m+k) + C_R(m-k).
LaTeX
$$$$ C_R(m) \\cdot C_R(k) = C_R(m+k) + C_R(m-k) $$$$
Lean4
/-- The product of two Chebyshev `C` polynomials is the sum of two other Chebyshev `C` polynomials.
-/
theorem C_mul_C (m k : ℤ) : C R m * C R k = C R (m + k) + C R (m - k) := by
induction k using Polynomial.Chebyshev.induct with
| zero => simp [mul_two]
| one => rw [C_add_one, C_one]; ring
| add_two k ih1 ih2 =>
have h₁ := C_add_two R (m + k)
have h₂ := C_sub_two R (m - k)
have h₃ := C_add_two R k
linear_combination (norm := ring_nf) C R m * h₃ - h₂ - h₁ - ih2 + (X : R[X]) * ih1
| neg_add_one k ih1 ih2 =>
have h₁ := C_add_two R (m + (-k - 1))
have h₂ := C_sub_two R (m - (-k - 1))
have h₃ := C_add_two R (-k - 1)
linear_combination (norm := ring_nf) C R m * h₃ - h₂ - h₁ - ih2 + (X : R[X]) * ih1
