Build_RightModuleIsomorphism' {R : Ring} (M N : RightModule R) (f : GroupIsomorphism M N) (p : forall r x, f (ract x r) = ract (f x) r) : RightModuleIsomorphism M N := Build_LeftModuleIsomorphism' (R:=rng_op R) M N f p.
Require Import WildCat. Require Import Spaces.Nat.Core. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Groups.Kernel Algebra.Groups.Image Algebra.Groups.QuotientGroup. Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct. Require Import Rings.Ring.