Commit 2023-08-29 08:16 1680acb6

View on Github →

feat: the category of presheaves of modules is preadditive (#6837)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

added theorem PresheafOfModules.Hom.add_app

modified def PresheafOfModules.Hom.app

added theorem PresheafOfModules.Hom.comp_app

modified theorem PresheafOfModules.Hom.ext

added theorem PresheafOfModules.Hom.neg_app

added theorem PresheafOfModules.Hom.sub_app

added theorem PresheafOfModules.Hom.zero_app

added theorem PresheafOfModules.toPresheaf_map_app