Def PresheafOfModules.evaluationJointlyReflectsColimits

Modification history

2024-05-08 15:35

Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean

feat(Algebra/Category/ModuleCat): the category of presheaves of modules has colimits (#12713)

Added PresheafOfModules.evaluationJointlyReflectsColimits View on Github →