mapPiEvalRingHom_comp_algebraMap — Mathlib

English

The composed maps satisfy: (mapPiEvalRingHom I) ∘ algebraMap = algebraMap ∘ Pi.evalRingHom R i.

Русский

Составленные отображения удовлетворяют: (mapPiEvalRingHom I) ∘ algebraMap = algebraMap ∘ Pi.evalRingHom R i.

LaTeX

$$$(\\mathrm{mapPiEvalRingHom}\\ I) \\circ (\\mathrm{algebraMap}\\_ { } ) = (\\mathrm{algebraMap}\\_ { } ) \\circ (\\Pi.evalRingHom R i)$$$

Lean4

theorem mapPiEvalRingHom_comp_algebraMap :
    (mapPiEvalRingHom I).comp (algebraMap _ _) = (algebraMap _ _).comp (Pi.evalRingHom R i) :=
  IsLocalization.map_comp _

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