Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-19 23:11 7013e5b7

View on Github →

feat(category_theory/internal): commutative monoid objects (#4186) This reprises a series of our recent PRs on monoid objects in monoidal categories, developing the same material for commutative monoid objects in braided categories.

Estimated changes

added theorem CommMon_.comp_hom
added theorem CommMon_.id_hom
added def CommMon_.trivial
added structure CommMon_
added theorem Mod.assoc_flip
added def Mod.comap
added def Mod.comp
added theorem Mod.comp_hom'
added def Mod.forget
added structure Mod.hom
added def Mod.id
added theorem Mod.id_hom'
added def Mod.regular
added structure Mod
deleted theorem Mod.assoc_flip
deleted def Mod.comap
deleted def Mod.comp
deleted theorem Mod.comp_hom'
deleted def Mod.forget
deleted structure Mod.hom
deleted def Mod.id
deleted theorem Mod.id_hom'
deleted def Mod.regular
deleted structure Mod