Theorem CategoryTheory.MorphismProperty.structuredArrowObj_iff

Modification history

2025-10-02 15:01
Mathlib/CategoryTheory/MorphismProperty/Comma.lean
feat(CategoryTheory/Limits/MorphismProperty): dualise lemmas on limits (#30127) …
Added CategoryTheory.MorphismProperty.structuredArrowObj_iffView on Github →