ringCatIsoToRingEquiv_toRingHom — Mathlib

English

From an isomorphism e in the RingCat, one obtains a RingEquiv between the underlying rings.

Русский

По изоморфизму e в RingCat получается кольцевое эквивалентное отображение между базовыми кольцами.

LaTeX

$$$\forall R,S:\text{RingCat},\; e:R\cong S \Rightarrow R.carrier \cong_{\mathsf{Ring}} S.carrier$$

Lean4

@[simp]
theorem ringCatIsoToRingEquiv_toRingHom {R S : RingCat.{u}} (e : R ≅ S) :
    (e.ringCatIsoToRingEquiv : R →+* S) = e.hom.hom :=
  rfl

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