Theorem CategoryTheory.CostructuredArrow.mkPrecomp_id

Modification history

2025-01-05 22:19
Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
chore: replace `aesop` with `simp` where possible (#20483) …
Modified CategoryTheory.CostructuredArrow.mkPrecomp_idView on Github →
2024-02-05 10:10
Mathlib/CategoryTheory/Comma/StructuredArrow.lean
feat: trivial morphisms in StructuredArrow (#10244)
Added CategoryTheory.CostructuredArrow.mkPrecomp_idView on Github →