Def ModuleCat.forget₂AddCommGroupPreservesLimitsAux

Modification history

2024-03-24 13:55
Mathlib/Algebra/Category/ModuleCat/Limits.lean
refactor(Algebra/Category): replace `TypeMax` constructions by `UnivLE` assumptions (#11420) …
Modified ModuleCat.forget₂AddCommGroupPreservesLimitsAuxView on Github →
2023-06-06 14:18
Mathlib/Algebra/Category/ModuleCat/Limits.lean
feat: port Algebra.Category.Module.Colimits (#4282)
Modified ModuleCat.forget₂AddCommGroupPreservesLimitsAuxView on Github →
2023-05-24 22:02
Mathlib/Algebra/Category/ModuleCat/Limits.lean
feat: port Algebra.Category.Module.Limits (#4297)
Added ModuleCat.forget₂AddCommGroupPreservesLimitsAuxView on Github →