coe_mapAlgHom_eq_coe_map — Mathlib

English

The underlying function of mapAlgHom is the same as the corresponding map on RatFunc, i.e., the coefficients coincide.

Русский

Функция wоуратного отображения mapAlgHom совпадает с соответствующим отображением на RatFunc.

LaTeX

$$$ (\operatorname{mapAlgHom} \varphi h_\varphi) = (\operatorname{map} \varphi h_\varphi) $$$

Lean4

theorem coe_mapAlgHom_eq_coe_map (φ : K[X] →ₐ[S] R[X]) (hφ : K[X]⁰ ≤ R[X]⁰.comap φ) :
    (mapAlgHom φ hφ : RatFunc K → RatFunc R) = map φ hφ :=
  rfl

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