Commit 2026-03-02 09:57 6e128b28
View on Github →feat(CategoryTheory/Triangulated): Rotated octahedron axiom (#35496)
This PR adds an alternative version of the octahedron axiom in triangulated categories, where all triangles have been rotated. This is similar to how distinguished_cocone_triangle₁ is a rotated version of distinguished_cocone_triangle.
I also added diagrams to the docstrings of both Octahedron and Octahedron'.