Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-16 11:02 05e7be9d

View on Github →

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

Estimated changes

Modified src/algebra/category/Module/limits.lean

added def Module.direct_limit_cocone

added def Module.direct_limit_diagram

added def Module.direct_limit_is_colimit