map_S — Mathlib

English

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

Русский

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

LaTeX

$$$ map\ f\ (S_R\ n) = S_{R'}(n) $$$

Lean4

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

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