Theorem CategoryTheory.Equivalence.trans_toAdjunction

Modification history

2025-12-13 14:21
Mathlib/CategoryTheory/Adjunction/Basic.lean
chore: use `Category*` everywhere (#32842) …
Modified CategoryTheory.Equivalence.trans_toAdjunctionView on Github →
2024-12-14 10:55
Mathlib/CategoryTheory/Adjunction/Basic.lean
feat(CategoryTheory/Monoidal): composition of monoidal category adjunctions (#17956) …
Added CategoryTheory.Equivalence.trans_toAdjunctionView on Github →