Commit 2023-04-08 22:23 3c7c29df

View on Github →

feat: port CategoryTheory.Triangulated.Rotate (#3047)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Triangulated/Rotate.lean

added def CategoryTheory.Pretriangulated.Triangle.invRotate

added def CategoryTheory.Pretriangulated.Triangle.rotate

added def CategoryTheory.Pretriangulated.invRotCompRot

added def CategoryTheory.Pretriangulated.invRotate

added def CategoryTheory.Pretriangulated.rotCompInvRot

added def CategoryTheory.Pretriangulated.rotate

added def CategoryTheory.Pretriangulated.triangleRotation