Commit 2023-03-09 14:54 61d9f573

View on Github →

feat: port CategoryTheory.Preadditive.FunctorCategory (#2746)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/FunctorCategory.lean

added def CategoryTheory.NatTrans.appHom

added theorem CategoryTheory.NatTrans.app_add

added theorem CategoryTheory.NatTrans.app_neg

added theorem CategoryTheory.NatTrans.app_nsmul

added theorem CategoryTheory.NatTrans.app_sub

added theorem CategoryTheory.NatTrans.app_sum

added theorem CategoryTheory.NatTrans.app_zero

added theorem CategoryTheory.NatTrans.app_zsmul