Lemma islinearinvmap {R} {M N : module R} (f : moduleiso M N) : islinear (invmap f). 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids.