IsLeftModule R (abgroup_vector M n). Proof. snrapply Build_IsLeftModule. - exact vector_lact. - exact left_heterodistribute_vector_lact_plus. - exact right_heterodistribute_vector_lact_plus. - exact heteroassociative_vector_lact_plus. - exact left_identity_vector_lact. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.PathGroupoids. Require Import Types.Sigma. Require Import Algebra.AbGroups.AbelianGroup Algebra.Rings.Ring Algebra.Rings.Module. Require Import Spaces.Nat.Core. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import abstract_algebra.