Def CategoryTheory.MonoOver.pullbackObjIsoOfIsPullback

Modification history

2025-03-11 16:03
Mathlib/CategoryTheory/Subobject/MonoOver.lean
feat(CategoryTheory/Subobject): add some lemmas wrt. the IsPullback API (#22379) …
Added CategoryTheory.MonoOver.pullbackObjIsoOfIsPullbackView on Github →