instIsLocalHomCarrierRingHomHomHomCommRingCat

English

If e: R ≅ S is an isomorphism of commutative rings, then the corresponding ring homomorphism e.hom is a local homomorphism.

Русский

Если e: R ≅ S — изоморфизм коммутативных колец, то соответствующий гомоморфизм колец e.hom является локальной гомоморфией.

LaTeX

$$$IsLocalHom\ (e.hom.hom)$$$

Lean4

instance {R S : CommRingCat} (e : R ≅ S) : IsLocalHom e.hom.hom :=
  isLocalHom_of_isIso _

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