proposition: Lemma islinearinvmap {R} {M N : module R} (f : moduleiso M N) : islinear (invmap f).
proof: Proof. intros r x. apply (invmaponpathsweq f). transitivity (module_mult N r x). exact (homotweqinvweq f (module_mult N r x)). transitivity (module_mult N r (moduleiso_to_weq f (invmap (moduleiso_to_weq f) x))). rewrite (homotweqinvweq (moduleiso_to_weq f) x). apply idpath. apply pathsinv0. apply (pr2 (moduleiso_ismodulefun f) r (invmap f x)). Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids