Theorem CategoryTheory.StructuredArrow.mkPostcomp_comp

Modification history

2024-02-05 10:10
Mathlib/CategoryTheory/Comma/StructuredArrow.lean
feat: trivial morphisms in StructuredArrow (#10244)
Added CategoryTheory.StructuredArrow.mkPostcomp_compView on Github →