Commit 2023-04-03 09:47 ee6812d4

View on Github →

feat: port CategoryTheory.Triangulated.Basic (#3046)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Triangulated/Basic.lean

added def CategoryTheory.Pretriangulated.Triangle.homMk

added theorem CategoryTheory.Pretriangulated.Triangle.hom_ext

added def CategoryTheory.Pretriangulated.Triangle.isoMk

added def CategoryTheory.Pretriangulated.Triangle.mk

added structure CategoryTheory.Pretriangulated.Triangle

added def CategoryTheory.Pretriangulated.TriangleMorphism.comp

added structure CategoryTheory.Pretriangulated.TriangleMorphism

added def CategoryTheory.Pretriangulated.contractibleTriangle

added def CategoryTheory.Pretriangulated.triangleMorphismId