Def CategoryTheory.AB4.ofAB5

Modification history

2024-11-19 08:25
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
refactor(CategoryTheory): make PreservesLimit and ReflectsLimit props (#19206) …
Deleted CategoryTheory.AB4.ofAB5View on Github →
2024-11-10 14:44
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
chore(CategoryTheory/Abelian/GrothendieckAxioms): remove unnecessary premise, clarify definition of AB4/5 (#18810) …
Modified CategoryTheory.AB4.ofAB5View on Github →
2024-10-22 18:49
Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean
feat(CategoryTheory/Abelian): AB5 implies AB4 (#17406) …
Added CategoryTheory.AB4.ofAB5View on Github →