mathlib documentation

category_theory.abelian.projective

Abelian categories with enough projectives have projective resolutions #

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

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