proposition: Lemma z_iso_moduleiso (M N : ob mod_category) : z_iso M N -> moduleiso M N.
proof: Proof. intro f. use make_moduleiso. - use make_weq. + exact (pr1modulefun (morphism_from_z_iso _ _ f)). + exact (moduleisweq_z_iso f). - exact (modulefun_ismodulefun (morphism_from_z_iso _ _ f)). Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.Algebra.Modules UniMath.Algebra.Modules.Examples UniMath.CategoryTheory.Limits.Zero