Def CategoryTheory.Over.opToUnderOp

Modification history

2025-10-31 08:47
Mathlib/CategoryTheory/Comma/Over/Basic.lean
chore: remove declarations deprecated before 2025-04-21 (#30759) …
Deleted CategoryTheory.Over.opToUnderOpView on Github →
2025-04-09 15:25
Mathlib/CategoryTheory/Comma/Over/Basic.lean
refactor: don't expose the functor `(Over X)ᵒᵖ ⥤ Under (op X)` (#23839) …
Modified CategoryTheory.Over.opToUnderOpView on Github →
2024-11-24 10:18
Mathlib/CategoryTheory/Comma/Over.lean
feat(CategoryTheory/Over): more API for `post` (#19312)
Added CategoryTheory.Over.opToUnderOpView on Github →