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