Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-09 12:24 fe5d6604

View on Github →

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!

Estimated changes