Build_LeftModuleIsomorphism' {R : Ring} (M N : LeftModule R) (f : GroupIsomorphism M N) (p : forall r x, f (r *L x) = r *L f x) : LeftModuleIsomorphism M N. Proof. snrapply Build_LeftModuleIsomorphism. - snrapply Build_LeftModuleHomomorphism. + exact f. + exact p. - exact _. Defined.
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.