Def CategoryTheory.Under.pullbackComp

Modification history

2025-04-15 15:31

Mathlib/CategoryTheory/Comma/Over/Pullback.lean

chore(CategoryTheory/Over): fix name of `Under.pullbackComp` (#24084)

Deleted CategoryTheory.Under.pullbackComp View on Github →

2024-07-17 18:39

Mathlib/CategoryTheory/Adjunction/Over.lean

deduplicate pullback and baseChange (#14519) …

Added CategoryTheory.Under.pullbackComp View on Github →