Theorem CategoryTheory.MorphismProperty.Comma.eqToHom_right

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.Comma.eqToHom_rightView on Github →