C_neg — Mathlib

English

Chebyshev C is even: C_R(−n) = C_R(n) for all integers n.

Русский

Полином Чебышёва C чётный по отношению к n: C_R(−n) = C_R(n) для всех целых n.

LaTeX

$$$ C_R(-n) = C_R(n) $$$

Lean4

@[simp]
theorem C_neg (n : ℤ) : C R (-n) = C R n := by
  induction n using Polynomial.Chebyshev.induct with
  | zero => rfl
  | one => simp only [C_neg_one, C_one]
  | add_two n ih1 ih2 =>
    have h₁ := C_add_two R n
    have h₂ := C_sub_two R (-n)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 - h₁ + h₂
  | neg_add_one n ih1 ih2 =>
    have h₁ := C_add_one R n
    have h₂ := C_sub_one R (-n)
    linear_combination (norm := ring_nf) (X : R[X]) * ih1 - ih2 + h₁ - h₂

Похожие утверждения