Commit 2023-03-21 21:39 2efe923b

View on Github →

feat: port CategoryTheory.SingleObj (#3021)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/SingleObj.lean

added theorem CategoryTheory.SingleObj.comp_as_mul

added def CategoryTheory.SingleObj.differenceFunctor

added theorem CategoryTheory.SingleObj.id_as_one

added theorem CategoryTheory.SingleObj.inv_as_inv

added def CategoryTheory.SingleObj.mapHom

added theorem CategoryTheory.SingleObj.mapHom_comp

added theorem CategoryTheory.SingleObj.mapHom_id

added def CategoryTheory.SingleObj.toEnd

added theorem CategoryTheory.SingleObj.toEnd_def

added def MonCat.toCat

added theorem MonoidHom.comp_toFunctor

added theorem MonoidHom.id_toFunctor

added def MonoidHom.toFunctor

added def Units.toAut

added theorem Units.toAut_hom

added theorem Units.toAut_inv