Theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.pushouts_ofLE_le_largerSubobject
Modification history
2025-02-21 13:27
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) …
Added CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.pushouts_ofLE_le_largerSubobjectView on Github →