Def CategoryTheory.Triangulated.someOctahedron

Modification history

2026-02-20 16:02

Mathlib/CategoryTheory/Triangulated/Triangulated.lean

chore(CategoryTheory/Triangulated): remove `someOctahedron'` (#35501) …

Modified CategoryTheory.Triangulated.someOctahedron View on Github →

2023-04-10 20:28

Mathlib/CategoryTheory/Triangulated/Triangulated.lean

feat: port CategoryTheory.Triangulated.Triangulated (#3072) …

Added CategoryTheory.Triangulated.someOctahedron View on Github →