Build_RingIsomorphism' (A B : Ring) (e : A <~> B) `{!IsSemiRingPreserving e} : RingIsomorphism A B := Build_RingIsomorphism A B (Build_RingHomomorphism e _) _.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.