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