Def ModuleCat.HasLimits.limitConeIsLimit

Modification history

2024-07-03 06:10
Mathlib/Algebra/Category/ModuleCat/Limits.lean
feat: the forget functor from ModuleCat to AddCommGrp reflects all limits (#14283) …
Modified ModuleCat.HasLimits.limitConeIsLimitView on Github →
2024-03-24 13:55
Mathlib/Algebra/Category/ModuleCat/Limits.lean
refactor(Algebra/Category): replace `TypeMax` constructions by `UnivLE` assumptions (#11420) …
Modified ModuleCat.HasLimits.limitConeIsLimitView on Github →
2023-06-06 14:18
Mathlib/Algebra/Category/ModuleCat/Limits.lean
feat: port Algebra.Category.Module.Colimits (#4282)
Modified ModuleCat.HasLimits.limitConeIsLimitView on Github →
2023-05-24 22:02
Mathlib/Algebra/Category/ModuleCat/Limits.lean
feat: port Algebra.Category.Module.Limits (#4297)
Added ModuleCat.HasLimits.limitConeIsLimitView on Github →