English
A ring isomorphism e: R ≃+* S induces an isomorphism in the category of semirings between of R and of S, with hom component of the iso given by ofHom e and inverse by ofHom e.symm.
Русский
Изоморфизм колец e: R ≃+* S индуцирует изоморфизм в категории полукольц между of R и of S, где компонентой гомоморфизма является ofHom e, а обратной компонентой — ofHom e.symm.
LaTeX
$$$ \mathrm{toSemiRingCatIso}(e) : \mathrm{of}(R) \cong \mathrm{of}(S) \quad \text{with }\; \mathrm{hom} = \mathrm{ofHom}(e),\; \mathrm{inv} = \mathrm{ofHom}(e^{-1}). $$$
Lean4
/-- Ring equivalences are isomorphisms in category of semirings -/
@[simps]
def _root_.RingEquiv.toSemiRingCatIso {R S : Type u} [Semiring R] [Semiring S] (e : R ≃+* S) : of R ≅ of S
where
hom := ofHom e
inv := ofHom e.symm
