Commit 2023-03-21 12:35 65db32fa

View on Github →

feat: port Algebra.Category.Mon.Basic (#2902)

Estimated changes

added theorem CommMonCat.Hom.map_mul
added theorem CommMonCat.Hom.map_one
added theorem CommMonCat.coe_of
added def CommMonCat.of
added def CommMonCat.ofHom
added theorem CommMonCat.ofHom_apply
added def CommMonCat
added theorem MonCat.Hom.map_mul
added theorem MonCat.Hom.map_one
added def MonCat.Hom.mk
added theorem MonCat.coe_of
added def MonCat.of
added def MonCat.ofHom
added theorem MonCat.ofHom_apply
added def MonCat