proposition: Lemma moduleiso_z_iso (M N : ob mod_category) : moduleiso M N -> z_iso M N.
proof: Proof. intro f. use make_z_iso'. - exact (moduleiso_to_modulefun f). - exact (moduleiso_is_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