map_U — Mathlib

English

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

Русский

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

LaTeX

$$$ map\ f\ (U_R\ n) = U_{R'}(n) $$$

Lean4

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

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