Theorem ModuleCat.enoughInjectives

Modification history

2024-10-26 23:35
Mathlib/Algebra/Category/ModuleCat/EnoughInjectives.lean
chore: do not depend on CategoryTheory in Module.Injective (#17747) …
Modified ModuleCat.enoughInjectivesView on Github →
2023-11-29 19:15
Mathlib/Algebra/Category/ModuleCat/Injective.lean
feat: category of $R$-modules has enough injectives (#7392)
Added ModuleCat.enoughInjectivesView on Github →