Commit 2023-04-09 07:30 7663224f

View on Github →

feat: port CategoryTheory.Triangulated.Pretriangulated (#3070)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean

added theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₁₂

added theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₂₃

added theorem CategoryTheory.Pretriangulated.comp_dist_triangle_mor_zero₃₁

added theorem CategoryTheory.Pretriangulated.inv_rot_of_dist_triangle

added theorem CategoryTheory.Pretriangulated.rot_of_dist_triangle