toCommSemiRingCatIso — Mathlib

English

Any ring equivalence e: R ≃+* S between commutative semirings induces an isomorphism in the category of commutative semirings between the corresponding objects ∘ R and ∘ S.

Русский

Любое эквивалентное соответствие колец e: R ≃+* S между коммутативными полукольцами порождает изоморфизм в категории коммутативных полукольц между соответствующими объектами.

LaTeX

$$$\text{RingEquiv}(R,S) \Rightarrow (\text{of }R) \cong (\text{of }S) \text{ in } CommSemiRingCat$$$

Lean4

/-- Ring equivalences are isomorphisms in category of commutative semirings -/
@[simps]
def _root_.RingEquiv.toCommSemiRingCatIso {R S : Type u} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : of R ≅ of S
    where
  hom := ofHom e
  inv := ofHom e.symm

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