English
The map mapAlg is the algebra homomorphism from R[X] to S[X] induced by the base map R → S.
Русский
Отображение mapAlg есть алгеброгомоморфизм из R[X] в S[X], индуцированный отображением основы R → S.
LaTeX
$$$$mapAlg\ R\ S\; p = map(\mathrm{algebraMap}\; R\ S)\; p.$$$$
Lean4
/-- The map `R[X] → S[X]` as an algebra homomorphism. -/
def mapAlg (R : Type u) [CommSemiring R] (S : Type v) [Semiring S] [Algebra R S] : R[X] →ₐ[R] S[X] :=
@aeval _ S[X] _ _ _ (X : S[X])