Commit 2023-04-25 11:14 26e27864

View on Github →

feat: port CategoryTheory.Preadditive.Generator (#3644)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/Generator.lean

added theorem CategoryTheory.Preadditive.isCoseparating_iff

added theorem CategoryTheory.Preadditive.isCoseparator_iff

added theorem CategoryTheory.Preadditive.isSeparating_iff

added theorem CategoryTheory.Preadditive.isSeparator_iff

added theorem CategoryTheory.isCoseparator_iff_faithful_preadditiveYoneda

added theorem CategoryTheory.isCoseparator_iff_faithful_preadditiveYonedaObj

added theorem CategoryTheory.isSeparator_iff_faithful_preadditiveCoyoneda

added theorem CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj