Def CategoryTheory.Triangulated.Octahedron.triangleMorphism₁

Modification history

2024-05-17 19:31

Mathlib/CategoryTheory/Triangulated/Triangulated.lean

style: remove all isolated `where` (#12991)

Modified CategoryTheory.Triangulated.Octahedron.triangleMorphism₁ View on Github →

2023-04-10 20:28

Mathlib/CategoryTheory/Triangulated/Triangulated.lean

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

Added CategoryTheory.Triangulated.Octahedron.triangleMorphism₁ View on Github →