Commit 2023-02-14 11:49 4f5c130c

View on Github →

feat: port CategoryTheory.Comma (#2260)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Comma.lean

added theorem CategoryTheory.Comma.comp_left

added theorem CategoryTheory.Comma.comp_right

added theorem CategoryTheory.Comma.eqToHom_left

added theorem CategoryTheory.Comma.eqToHom_right

added def CategoryTheory.Comma.fst

added theorem CategoryTheory.Comma.hom_ext

added theorem CategoryTheory.Comma.id_left

added theorem CategoryTheory.Comma.id_right

added def CategoryTheory.Comma.isoMk

added def CategoryTheory.Comma.mapLeft

added def CategoryTheory.Comma.mapLeftComp

added def CategoryTheory.Comma.mapLeftId

added def CategoryTheory.Comma.mapRight

added def CategoryTheory.Comma.mapRightComp

added def CategoryTheory.Comma.mapRightId

added def CategoryTheory.Comma.natTrans

added def CategoryTheory.Comma.post

added def CategoryTheory.Comma.preLeft

added def CategoryTheory.Comma.preRight

added def CategoryTheory.Comma.snd

added structure CategoryTheory.Comma

added structure CategoryTheory.CommaMorphism