Commit 2021-04-09 12:24 fe5d6604

feat(algebra/category/Module): arbitrary colimits (#7099) This is just the "semi-automated" construction of arbitrary colimits in the category or R-modules, following the same model as for Mon, AddCommGroup, etc. We already have finite colimits from the abelian instance. One could also give definitionally nicer colimits as quotients of finitely supported functions. But this is better than nothing!