Commit 2025-02-17 08:13 981a86e7

View on Github →

fix(CategoryTheory): fix incorrectly ported declaration (#21918) The two declarations in Yoneda/Projective.lean were actually identical due to what I assume is a mistake during the port.

Estimated changes

Modified Mathlib/CategoryTheory/Abelian/Projective.lean

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

added theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj

deleted theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj'