Theorem CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fst

Modification history

2025-12-03 07:14
Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
refactor: MorphismProperty.HasPullbacksAlong (#31231) …
Modified CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fstView on Github →
2025-10-15 15:17
Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
refactor: weaken HasPullbacks to HasPullback in MorphismProperty.OverAdjuction (#29810) …
Modified CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fstView on Github →
2024-11-27 11:40
Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
feat(CategoryTheory): pushforward pullback adjunction for `P.Over Q X` (#19271)
Added CategoryTheory.MorphismProperty.Over.pullbackComp_left_fst_fstView on Github →