Mathlib v3 is deprecated. Go to Mathlib v4

Def Module.colimits.colimit_type

Modification history

2022-02-03 18:39
src/algebra/category/Module/colimits.lean
fix(algebra/category/Module/colimits): generalize universes (#11802)
Modified Module.colimits.colimit_typeView on Github →
2021-04-09 12:24
src/algebra/category/Module/colimits.lean
feat(algebra/category/Module): arbitrary colimits (#7099) …
Added Module.colimits.colimit_typeView on Github →