Def ModuleCat.Colimits.descFun

Modification history

2023-09-04 16:01
Mathlib/Algebra/Category/ModuleCat/Colimits.lean
refactor: colimits in ModuleCat (#6925) …
Deleted ModuleCat.Colimits.descFunView on Github →
2023-06-06 14:18
Mathlib/Algebra/Category/ModuleCat/Colimits.lean
feat: port Algebra.Category.Module.Colimits (#4282)
Added ModuleCat.Colimits.descFunView on Github →