Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-26 08:06 5c93c2d0

View on Github →

feat(category_theory/triangulated/rotate): add definition of rotation and inverse rotation of triangles and their morphisms (#6803) This PR adds the definition of rotation and inverse rotation of triangles and triangle morphisms. It also shows that rotation is an equivalence on the category of triangles in an additive category.

Estimated changes