Theorem CategoryTheory.IsGrothendieckAbelian.subobject_mk_of_isColimit_eq_iSup

Modification history

2025-02-20 13:00
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean
feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) …
Deleted CategoryTheory.IsGrothendieckAbelian.subobject_mk_of_isColimit_eq_iSupView on Github →
2025-02-17 13:55
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean
feat(CategoryTheory): subobjects in Grothendieck abelian categories (#21986) …
Added CategoryTheory.IsGrothendieckAbelian.subobject_mk_of_isColimit_eq_iSupView on Github →