Commit 2023-09-22 17:59 3430a1fb

View on Github →

feat: definition of the distinguished triangles in the opposite category (#7327)

Estimated changes

Modified Mathlib/CategoryTheory/Opposites.lean

Modified Mathlib/CategoryTheory/Triangulated/Opposite.lean

added def CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles

added theorem CategoryTheory.Pretriangulated.Opposite.isomorphic_distinguished

added theorem CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff'

added theorem CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff