Theorem CategoryTheory.Functor.commShiftIso_id_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_id_inv_app View on Github →

2024-07-01 14:30

Mathlib/CategoryTheory/Shift/CommShift.lean

feat(CategoryTheory/Shift): more compatibilities for NatTrans.CommShift (#14187) …

Added CategoryTheory.Functor.commShiftIso_id_inv_app View on Github →