Theorem CategoryTheory.CostructuredArrow.mkPrecomp_comp

Modification history

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