Theorem CategoryTheory.Functor.hasZeroObject_of_additive

Modification history

2024-06-06 14:57
Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean
feat(CategoryTheory): localization of triangulated categories (#11786) …
Added CategoryTheory.Functor.hasZeroObject_of_additiveView on Github →