map_wittPolynomial — Mathlib

English

Let f: R →+* S be a ring homomorphism. Then applying f to the Witt polynomial yields the Witt polynomial over S: map f (W_p,R,n) = W_p,S,n for all n.

Русский

Пусть f: R →+* S — кольцевой гомоморфизм. Тогда отображение коэффициентов отправляет Witt-полиномy в Witt-полиномy над S: map f (W_p,R,n) = W_p,S,n для всех n.

LaTeX

$$$ map\ f\ (W_p\ R\ n) = W_p\ S\ n $$$

Lean4

@[simp]
theorem map_wittPolynomial (f : R →+* S) (n : ℕ) : map f (W n) = W n :=
  by
  rw [wittPolynomial, map_sum, wittPolynomial]
  refine sum_congr rfl fun i _ => ?_
  rw [map_monomial, RingHom.map_pow, map_natCast]

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