mapAlg_eq_map — Mathlib

English

mapAlg is the morphism induced by the base map R → S, i.e., mapAlg p = map(algebraMap R S) p.

Русский

mapAlg есть отображение, индуцированное отображением основы R → S, то есть mapAlg p = map(algebraMap R S) p.

LaTeX

$$$$\mathrm{mapAlg}\ R\ S\; p = \mathrm{map}(\mathrm{algebraMap}\ R\ S)\; p.$$$$

Lean4

/-- `mapAlg` is the morphism induced by `R → S`. -/
theorem mapAlg_eq_map (S : Type v) [Semiring S] [Algebra R S] (p : R[X]) : mapAlg R S p = map (algebraMap R S) p := by
  rfl

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