# mathlibdocumentation

category_theory.abelian.projective

# Abelian categories with enough projectives have projective resolutions #

When C is abelian projective.d f and f are exact.

theorem category_theory.exact_d_f {C : Type u} {X Y : C} (f : X Y) :

When C is abelian, projective.d f and f are exact.