map_C — Mathlib

English

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

Русский

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

LaTeX

$$$ map\ f\ (C_R\ n) = C_{R'}(n) $$$

Lean4

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

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