English
Polynomial.mapRingHom(f) defines a ring hom from polynomial ring R[X] to S[X], with toFun = map f and compatibility with all ring operations.
Русский
Polynomial.mapRingHom(f) задаёт кольцевой гомоморфизм от кольцевой оболочки R[X] к S[X], при этом toFun = map f и сохранение всех операций кольца.
LaTeX
$$$$\\operatorname{mapRingHom}(f) : R[X] \\to^+ S[X],\\; \\text{toFun} = \\mathrm{map}\, f,\\; \\text{map\_add}' = \\mathrm{map\_add}\, f,\\; \\text{map\_zero}' = \\mathrm{map\_zero}\, f,\\; \\text{map\_mul}' = \\mathrm{map\_mul}\, f,\\; \\text{map\_one}' = \\mathrm{map\_one}\, f.$$$$
Lean4
/-- `Polynomial.map` as a `RingHom`. -/
def mapRingHom (f : R →+* S) : R[X] →+* S[X]
where
toFun := Polynomial.map f
map_add' _ _ := Polynomial.map_add f
map_zero' := Polynomial.map_zero f
map_mul' _ _ := Polynomial.map_mul f
map_one' := Polynomial.map_one f
