fact: Definition mult_to_module {R : ring} {G : abgr} {m : R -> G -> G} (ax1 : mult_isldistr_wrt_grop m) (ax2 : mult_isrdistr_wrt_ringop1 m) (ax3 : mult_isrdistr_wrt_ringop2 m) (ax4 : mult_unel m) : module R := make_module G (mult_to_module_struct ax1 ax2 ax3 ax4).
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids