Theorem CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_app

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.shift_opShiftFunctorEquivalence_counitIso_inv_appView on Github →
2025-12-10 21:53
Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean
feat(CategoryTheory): the opposite of a triangulated category is triangulated (#32535)
Added CategoryTheory.Pretriangulated.shift_opShiftFunctorEquivalence_counitIso_inv_appView on Github →