Structures · Category theory
CategoryTheory.IsCommMonObj
Predicate for a monoid object to be commutative.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Mon
- Shape
- One type argument · adds mul_comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances4
- CategoryTheory.Over
- CategoryTheory.Grp
- CategoryTheory.Mon
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by46
- CategoryTheory.IsCommMonObj.mul_comm
- CategoryTheory.CommGrp.mkIso'
- CategoryTheory.CommMon.mkIso'
- CategoryTheory.IsCommMonObj.mul_comm'
- CategoryTheory.Hom.commGroup
- CategoryTheory.MonObj.mul_mul_mul_comm'
- CategoryTheory.MonObj.mul_mul_mul_comm
- CategoryTheory.Grp.Hom.hom_pow
- CategoryTheory.Mon.Hom.hom_pow
- CategoryTheory.instIsMonHomInvOfIsCommMonObj
- CategoryTheory.Mon.Hom.hom_mul
- CategoryTheory.Mon.hom_one
- CategoryTheory.Grp.Hom.hom_one
- CategoryTheory.Grp.Hom.hom_mul
- CategoryTheory.CommGrp.mkIso'_inv_hom_hom_hom
- CategoryTheory.Grp.instGrpObj
- CategoryTheory.MonObj.instIsMonHomMulOfIsCommMonObj
- CategoryTheory.CommMon.mkIso'_inv_hom_hom
- CategoryTheory.Grp.Hom.hom_hom_div
- CommMonTypeEquivalenceCommMon.commMonCommMonoid
- CategoryTheory.Mon.hom_mul
- CategoryTheory.IsMonHom.instNormalOfIsCommMonObjOfMono
- CategoryTheory.Mon.instIsCommMonObj
- CategoryTheory.MonObj.mul_mul_mul_comm_assoc
- CategoryTheory.Mon.Hom.hom_one
- CategoryTheory.MonObj.mul_mul_mul_comm'_assoc
- CategoryTheory.IsCommMonObj.mul_comm'_assoc
- AlgebraicGeometry.Scheme.isCommMonObj_asOver_pullback
- CategoryTheory.GrpObj.conj_eq_snd_of_isCommMonObj
- CategoryTheory.Hom.commMonoid
- CategoryTheory.CommGrp.mkIso'_hom_hom_hom_hom
- CategoryTheory.Over.isCommMonObj_mk_pullbackSnd
- CategoryTheory.Functor.isCommMonObj_obj
- CommGrpTypeEquivalenceCommGrp.commGrpCommGroup
- CategoryTheory.Grp.hom_mul
- CategoryTheory.instIsMonHomInvHomOfIsCommMonObj
- CategoryTheory.Grp.instIsCommMonObj
- CategoryTheory.IsCommMonObj.mul_comm_assoc
- CategoryTheory.Mon.instMonObjOfIsCommMonObjX
- CategoryTheory.Grp.instMonObj
- CategoryTheory.Grp.Hom.hom_hom_inv
- CategoryTheory.Grp.Hom.hom_hom_zpow
- CategoryTheory.Grp.instIsMonHom
- CategoryTheory.CommMon.mkIso'_hom_hom_hom
- CategoryTheory.Grp.hom_one
- CategoryTheory.instIsCommMonObjTensorObj
Ancestors0
No ancestors.