Commit 2024-02-19 20:27 eaaf5562
View on Github →feat(CategoryTheory/Triangulated): more API (#10527) In this PR, it is shown that in order to show that a pretriangulated category is triangulated category, i.e. in order to check the octahedron axiom, it is possible to replace a given diagram by an isomorphic diagram. This shall be used in #9550 in order to show that the homotopy category of cochain complexes in an additive category is triangulated.