mapPiEvalRingHom — Mathlib

English

Alternative expression of the previous composition equality.

Русский

Альтернативное выражение тождеству композиции.

LaTeX

$$$( (mapPiEvalRingHom I).comp (algebraMap _ _) ) = (algebraMap _ _).comp (Pi.evalRingHom R i).$$$

Lean4

/-- `Localization.localRingHom` specialized to a projection homomorphism from a product ring. -/
noncomputable abbrev mapPiEvalRingHom :
    Localization.AtPrime (I.comap <| Pi.evalRingHom R i) →+* Localization.AtPrime I :=
  localRingHom _ _ _ rfl

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