Build_RingIsomorphism'' (A B : Ring) (e : GroupIsomorphism A B) {H : IsMonoidPreserving (Aop:=ring_mult) (Bop:=ring_mult) (Aunit:=one) (Bunit:=one) e} : RingIsomorphism A B := @Build_RingIsomorphism' A B e (Build_IsSemiRingPreserving e _ H).
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.