Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-02-05 10:10
6d4aa853
View on Github →
feat: trivial morphisms in StructuredArrow (
#10244
)
Estimated changes
Modified
Mathlib/CategoryTheory/Comma/StructuredArrow.lean
added
def
CategoryTheory.CostructuredArrow.mkPrecomp
added
theorem
CategoryTheory.CostructuredArrow.mkPrecomp_comp
added
theorem
CategoryTheory.CostructuredArrow.mkPrecomp_id
added
def
CategoryTheory.StructuredArrow.mkPostcomp
added
theorem
CategoryTheory.StructuredArrow.mkPostcomp_comp
added
theorem
CategoryTheory.StructuredArrow.mkPostcomp_id