feat(category_theory/abelian): abelian categories with enough projectives have projective resolutions (#7488)
feat(category_theory/abelian): abelian categories with enough projectives have projective resolutions (#7488)




Co-authored-by: Scott Morrison <63f04b4d96235eb042cc46d94f14d241d2a26722@gmail.com>
Co-authored-by: Johan Commelin <759412786bc533369b22377bf83fb9056c5b25b2@commelin.net>

leanprover-community/mathlib,leanprover-community/mathlib