Theorem CategoryTheory.MorphismProperty.Under.Hom.ext

Modification history

2024-11-27 11:40

Mathlib/CategoryTheory/MorphismProperty/Comma.lean

feat(CategoryTheory): pushforward pullback adjunction for `P.Over Q X` (#19271)

Added CategoryTheory.MorphismProperty.Under.Hom.ext View on Github →