Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Module.colimits.cocone_naturality_components

Modification history

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