T_eq_half_mul_C_comp_two_mul_X — Mathlib

English

Under the same invertibility assumption, C_R(n) equals 2 times the composition of T_R(n) with (C_R(1/2) · X).

Русский

При тех же предположениях об обратимости 2: C_R(n) = 2 · (T_R(n)) ∘ (C_R(1/2) · X).

LaTeX

$$$ C_R(n) = 2 \cdot (T_R(n)).comp (C_R(\tfrac{1}{2}) \cdot X) $$$

Lean4

theorem T_eq_half_mul_C_comp_two_mul_X [Invertible (2 : R)] (n : ℤ) : T R n = Polynomial.C ⅟2 * (C R n).comp (2 * X) :=
  by rw [C_comp_two_mul_X, ← mul_assoc, ← map_ofNat Polynomial.C 2, ← map_mul, invOf_mul_self', map_one, one_mul]

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