English
For a ring hom f : R →+* S, there is a polynomial map map f : R[X] → S[X], which is compatible with addition, multiplication, and constant terms, and sends X to X.
Русский
Для кольцевого гомоморфа f : R →+* S существует отображение полиномов map f : R[X] → S[X], сохраняющее сложение, умножение и константы, и такое, что X отправляется в X.
LaTeX
$$$$(\\operatorname{map} f)(p+q) = (\\operatorname{map} f p) + (\\operatorname{map} f q), \\\\ (\\operatorname{map} f)(p q) = (\\operatorname{map} f p)(\\operatorname{map} f q), \\\\ (\\operatorname{map} f)(C a) = C (f a), \\\\ (\\operatorname{map} f)(X) = X.$$$$
Lean4
/-- `map f p` maps a polynomial `p` across a ring hom `f` -/
def map : R[X] → S[X] :=
eval₂ (C.comp f) X
