Def CategoryTheory.Over.forgetAdjStar

Modification history

2025-04-09 12:22
Mathlib/CategoryTheory/Comma/Over/Pullback.lean
feat: the category over a terminal object (#23702) …
Modified CategoryTheory.Over.forgetAdjStarView on Github →
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.forgetAdjStarView on Github →