English
Let R be a commutative ring. The m n-th Chebyshev T polynomial is the composition of the m-th and n-th: T_R(m n) = (T_R m) ∘ (T_R n).
Русский
Пусть R — коммутативное кольцо. m n-й полином Чебышёва T является композиционным произведением m-й и n-й: T_R(m n) = (T_R m) ∘ (T_R n).
LaTeX
$$$$ T_R(m n) = (T_R m) \\circ (T_R n) $$$$
Lean4
/-- The `(m * n)`-th Chebyshev `T` polynomial is the composition of the `m`-th and `n`-th. -/
theorem T_mul (m n : ℤ) : T R (m * n) = (T R m).comp (T R n) := by
induction m using Polynomial.Chebyshev.induct with
| zero => simp
| one => simp
| add_two m ih1 ih2 =>
have h₁ := T_mul_T R ((m + 1) * n) n
have h₂ := congr_arg (comp · (T R n)) <| T_add_two R m
simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1
| neg_add_one m ih1 ih2 =>
have h₁ := T_mul_T R ((-m) * n) n
have h₂ := congr_arg (comp · (T R n)) <| T_add_two R (-m - 1)
simp only [sub_comp, mul_comp, ofNat_comp, X_comp] at h₂
linear_combination (norm := ring_nf) -ih2 - h₂ - h₁ + 2 * T R n * ih1
