Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-13 13:44 c5faeade

View on Github →

feat(category_theory/preadditive/functor_category): preadditive instance for C \func D (#7533)

Estimated changes

Modified src/category_theory/preadditive/default.lean

modified theorem category_theory.preadditive.comp_gsmul

added def category_theory.preadditive.comp_hom

modified theorem category_theory.preadditive.comp_neg

added theorem category_theory.preadditive.comp_nsmul

modified theorem category_theory.preadditive.comp_sub

modified theorem category_theory.preadditive.comp_sum

modified theorem category_theory.preadditive.gsmul_comp

modified theorem category_theory.preadditive.neg_comp

modified theorem category_theory.preadditive.neg_comp_neg

added theorem category_theory.preadditive.nsmul_comp

modified theorem category_theory.preadditive.sub_comp

modified theorem category_theory.preadditive.sum_comp

Created src/category_theory/preadditive/functor_category.lean

added theorem category_theory.nat_trans.app_add

added theorem category_theory.nat_trans.app_gsmul

added def category_theory.nat_trans.app_hom

added theorem category_theory.nat_trans.app_neg

added theorem category_theory.nat_trans.app_nsmul

added theorem category_theory.nat_trans.app_sub

added theorem category_theory.nat_trans.app_sum

added theorem category_theory.nat_trans.app_zero