Theorem CategoryTheory.Pretriangulated.shiftFunctor_op_map

Modification history

2025-12-12 17:53
Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean
feat(CategoryTheory/Triangulated): `opOp` and `unopUnop` commute with shifts (#32594) …
Modified CategoryTheory.Pretriangulated.shiftFunctor_op_mapView on Github →
2023-09-22 12:58
Mathlib/CategoryTheory/Triangulated/Opposite.lean
feat: the shift on the opposite category (#7324)
Added CategoryTheory.Pretriangulated.shiftFunctor_op_mapView on Github →