Commit 2023-05-25 17:59 a601ad1e

View on Github →

feat: port CategoryTheory.Abelian.Injective (#4348)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/Injective.lean

added theorem CategoryTheory.injective_of_preservesFiniteColimits_preadditiveYonedaObj

added def CategoryTheory.preservesFiniteColimitsPreadditiveYonedaObjOfInjective