Theorem CategoryTheory.Adjunction.CommShift.compatibilityCounit_unique_left

Modification history

2025-01-01 17:49
Mathlib/CategoryTheory/Shift/Adjunction.lean
feat(CategoryTheory/Shift/Adjunction): commutation with shifts and adjunctions, part 2 (#20273) …
Deleted CategoryTheory.Adjunction.CommShift.compatibilityCounit_unique_leftView 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.compatibilityCounit_unique_leftView on Github →