C_eq_two_mul_T_comp_half_mul_X — Mathlib

English

If 2 is invertible in R, then C_R(n) = 2 · (T_R(n)) ∘ (C_R(1/2) · X).

Русский

Пусть в кольце R число 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 C_eq_two_mul_T_comp_half_mul_X [Invertible (2 : R)] (n : ℤ) : C R n = 2 * (T R n).comp (Polynomial.C ⅟2 * X) :=
  by
  have := congr_arg (·.comp (Polynomial.C ⅟2 * X)) (C_comp_two_mul_X R n)
  simp_rw [comp_assoc, mul_comp, ofNat_comp, X_comp, ← mul_assoc, ← C_eq_natCast, ← C_mul, Nat.cast_ofNat,
    mul_invOf_self', map_one, one_mul, comp_X, map_ofNat] at this
  assumption

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