Def CategoryTheory.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) …
Deleted CategoryTheory.forgetAdjStarView on Github →
2023-04-21 08:03
Mathlib/CategoryTheory/Adjunction/Over.lean
feat: port CategoryTheory.Adjunction.Over (#3562)
Added CategoryTheory.forgetAdjStarView on Github →