Theorem CategoryTheory.Limits.hasColimits_of_hasLimits_of_hasCoseparator

Modification history

2024-12-16 16:45
Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
feat(CategoryTheory/Abelian/GrothendieckAxioms): introduce Grothendieck categories (#18510) …
Added CategoryTheory.Limits.hasColimits_of_hasLimits_of_hasCoseparatorView on Github →