Theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal
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.exists_ordinalView on Github →