Def CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso

Modification history

2025-12-12 17:53

Mathlib/CategoryTheory/Triangulated/Opposite/OpOp.lean

feat(CategoryTheory/Triangulated): `opOp` and `unopUnop` commute with shifts (#32594) …

Added CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso View on Github →