2025-02-20 13:00
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean
feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) …
Added CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup