Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-08-27 16:15
7a05c35f
View on Github →
feat: functoriality of StructuredArrow.homMk' (
#6813
)
Estimated changes
Modified
Mathlib/CategoryTheory/StructuredArrow.lean
added
theorem
CategoryTheory.CostructuredArrow.homMk'_comp
added
theorem
CategoryTheory.CostructuredArrow.homMk'_id
added
theorem
CategoryTheory.CostructuredArrow.homMk'_mk_comp
added
theorem
CategoryTheory.CostructuredArrow.homMk'_mk_id
added
theorem
CategoryTheory.StructuredArrow.eqToHom_right
added
theorem
CategoryTheory.StructuredArrow.homMk'_comp
added
theorem
CategoryTheory.StructuredArrow.homMk'_id
added
theorem
CategoryTheory.StructuredArrow.homMk'_mk_comp
added
theorem
CategoryTheory.StructuredArrow.homMk'_mk_id