Theorem CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso

Modification history

2024-12-19 17:27
Mathlib/CategoryTheory/Shift/Adjunction.lean
feat(CategoryTheory/Shift): commutation with shifts and adjunctions (#20033) …
Added CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_isoView on Github →