Theorem CategoryTheory.StructuredArrow.obj_ext

Modification history

2025-05-13 20:30
Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
feat(CategoryTheory/Limits/Final): `fromPUnit c` is final if `c` is terminal (#24847) …
Added CategoryTheory.StructuredArrow.obj_extView on Github →