algebraMap_apply — Mathlib

English

For any coefficient x ∈ R, the image of x under the algebra map to S equals the image of the constant polynomial x under h.map.

Русский

Для коэффициента x ∈ R образ отображения алгебры в S равен образу константного многочлена x под h.map.

LaTeX

$$$\\text{algebraMap}_{R,S}(x) = h.map(\\mathbf{C} x)$$$

Lean4

theorem algebraMap_apply (x : R) : algebraMap R S x = h.map (Polynomial.C x) :=
  AlgHom.algebraMap_eq_apply h.map rfl

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