Commit 2023-05-11 00:33 b5ac03c3

View on Github →

feat: port CategoryTheory.Preadditive.Yoneda.Projective (#3895)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/Yoneda/Projective.lean

added theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj

added theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditive_coyoneda_obj'