Commit 2023-03-29 00:39 d8d0c899

View on Github →

feat: port Algebra.Category.Group.Preadditive (#3144)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/GroupCat/Preadditive.lean

added theorem AddCommGroupCat.hom_add_apply

Modified Mathlib/CategoryTheory/Preadditive/Basic.lean