map_T — Mathlib

English

For any ring hom f, map f (T_R n) = T_{R'}(n).

Русский

Для любого кольцевого отображения f выполняется отображение T_R(n) в T_R'(n).

LaTeX

$$$ map\ f\ (T_R\ n) = T_{R'}(n) $$$

Lean4

@[simp]
theorem map_T (f : R →+* R') (n : ℤ) : map f (T R n) = T R' n := by
  induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp_rw [T_add_two, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1, ih2]
  | neg_add_one n ih1 ih2 =>
    simp_rw [T_sub_one, Polynomial.map_sub, Polynomial.map_mul, Polynomial.map_ofNat, map_X, ih1, ih2]

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