Theorem CategoryTheory.Adjunction.CommShift.mk'

Modification history

2025-11-17 00:03
Mathlib/CategoryTheory/Shift/Adjunction.lean
refactor(CategoryTheory/Shift): export Functor.CommShift.commShiftIso (#31504) …
Modified CategoryTheory.Adjunction.CommShift.mk'View on Github →
2024-12-19 17:27
Mathlib/CategoryTheory/Shift/Adjunction.lean
feat(CategoryTheory/Shift): commutation with shifts and adjunctions (#20033) …
Added CategoryTheory.Adjunction.CommShift.mk'View on Github →