mapAlg — Mathlib

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])

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