Theorem ModuleCat.hasLimit

Modification history

2024-04-20 20:51
Mathlib/Algebra/Category/ModuleCat/Limits.lean
feat(Algebra/Category/ModuleCat): the category of presheaves of modules has limits (#12264)
Deleted ModuleCat.hasLimitView on Github →
2024-03-24 13:55
Mathlib/Algebra/Category/ModuleCat/Limits.lean
refactor(Algebra/Category): replace `TypeMax` constructions by `UnivLE` assumptions (#11420) …
Added ModuleCat.hasLimitView on Github →