Commit 2021-03-10 11:57 eaa02185
View on Github →feat(category_theory/triangulated/basic): add definitions of additive category and triangle (#6539) This PR adds the definition of an additive category and the definition of a triangle in an additive category with an additive shift.