Def CategoryTheory.Triangulated.someOctahedron'

Modification history

2026-03-02 09:57
Mathlib/CategoryTheory/Triangulated/Triangulated.lean
feat(CategoryTheory/Triangulated): Rotated octahedron axiom (#35496) …
Added CategoryTheory.Triangulated.someOctahedron'View on Github →
2026-02-20 16:02
Mathlib/CategoryTheory/Triangulated/Triangulated.lean
chore(CategoryTheory/Triangulated): remove `someOctahedron'` (#35501) …
Deleted 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 →