coe_mapRingHom_eq_coe_map — Mathlib

English

The two natural ways to view the map induced by a ring homomorphism are the same on RatFunc: coe of mapRingHom equals coe of map.

Русский

Два естественных способа задания отображения, индуцированного кольцевым гомоморфизмом, совпадают на RatFunc.

LaTeX

$$$\bigl(\mathrm{mapRingHom}\,\phi\,\mathrm{h}\phi\bigr) = \mathrm{map}\,\phi\,\mathrm{h}\phi$$$

Lean4

theorem coe_mapRingHom_eq_coe_map [RingHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap φ) :
    (mapRingHom φ hφ : RatFunc R → RatFunc S) = map φ hφ :=
  rfl

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