Theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eq

Modification history

2025-12-12 17:53
Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean
feat(CategoryTheory/Triangulated): `opOp` and `unopUnop` commute with shifts (#32594) …
Added CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_inv_app_eqView on Github →