Def CategoryTheory.Over.forgetAdjStar

Modification history

2024-05-19 09:37

Mathlib/CategoryTheory/Adjunction/Over.lean

feat: moving some adjunctions of over categories to `CategoryTheory.Adjunction.Over` (#12980) …

Added CategoryTheory.Over.forgetAdjStar View on Github →