Theorem CategoryTheory.Functor.commShiftIso_comp_inv_app

Modification history

2025-11-17 00:03

Mathlib/CategoryTheory/Shift/CommShift.lean

refactor(CategoryTheory/Shift): export Functor.CommShift.commShiftIso (#31504) …

Deleted CategoryTheory.Functor.commShiftIso_comp_inv_app View on Github →

2024-06-24 08:03

Mathlib/CategoryTheory/Shift/CommShift.lean

feat(CategoryTheory): more API for the commutation of functors with shifts (#13757) …

Added CategoryTheory.Functor.commShiftIso_comp_inv_app View on Github →