proposition: Lemma intersection_submodule {R : ring} {M : module R} {I : UU} (S : I -> hsubtype M) (each_is_submodule : ∏ i : I, issubmodule (S i)) : issubmodule (subtype_intersection S).
proof: Proof. intros. use make_issubmodule. - exact (intersection_subgr S (λ i, (pr1 (each_is_submodule i)))). - intros r m a i. exact (pr2 (each_is_submodule i) r m (a i)). Qed.
imports: UniMath.MoreFoundations.Subtypes UniMath.Algebra.RigsAndRings UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.Modules.Core