Def Module.direct_limit_cocone

Modification history

2021-01-16 11:02

src/algebra/category/Module/limits.lean

feat(algebra/category/Module): direct limit is a colimit (#4756)

Added Module.direct_limit_cocone View on Github →