2025-07-15 16:05
Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean
feat(CategoryTheory/Preadditive/Injective/Basic, CategoryTheory/Preadditive/Projective/Basic): injectivity/projectivity criterion (#27156) …
Added CategoryTheory.Functor.projective_of_map_projective