Commit 2023-04-10 20:28 c5372bb1

View on Github →

feat: port CategoryTheory.Triangulated.Triangulated (#3072) Also actually corrects the SHA that was incorrectly corrected in #3346; the stupid example was in CategoryTheory.Triangulated.Rotate and not CategoryTheory.Triangulated.Basic.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Triangulated/Basic.lean

Modified Mathlib/CategoryTheory/Triangulated/Rotate.lean

Created Mathlib/CategoryTheory/Triangulated/Triangulated.lean

added def CategoryTheory.Triangulated.Octahedron.triangle

added def CategoryTheory.Triangulated.Octahedron.triangleMorphism₁

added def CategoryTheory.Triangulated.Octahedron.triangleMorphism₂

added structure CategoryTheory.Triangulated.Octahedron

added def CategoryTheory.Triangulated.someOctahedron'

added def CategoryTheory.Triangulated.someOctahedron