Commit 2024-01-12 17:18 216d93e9

View on Github →

chore(CategoryTheory/SingleObj): unify notation (#9696) Use consistent notation for a monoid M, a group G, etc.

Estimated changes

Modified Mathlib/CategoryTheory/SingleObj.lean

modified theorem CategoryTheory.SingleObj.comp_as_mul

modified def CategoryTheory.SingleObj.differenceFunctor

modified def CategoryTheory.SingleObj.functor

modified theorem CategoryTheory.SingleObj.id_as_one

modified theorem CategoryTheory.SingleObj.inv_as_inv

modified def CategoryTheory.SingleObj.mapHom

modified theorem CategoryTheory.SingleObj.mapHom_comp

modified theorem CategoryTheory.SingleObj.mapHom_id

modified def CategoryTheory.SingleObj.natTrans

modified def CategoryTheory.SingleObj.toEnd

modified theorem CategoryTheory.SingleObj.toEnd_def

modified theorem MonoidHom.comp_toFunctor

modified theorem MonoidHom.id_toFunctor

modified def MonoidHom.toFunctor

modified def Units.toAut

modified theorem Units.toAut_hom

modified theorem Units.toAut_inv