Structures · Category theory
CategoryTheory.IsCommAddMonObj
Predicate for an additive monoid object to be commutative.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Mon
- Shape
- One type argument · adds add_comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances2
- CategoryTheory.AddGrp
- CategoryTheory.AddMon
How is a type an instance?
Loading the hierarchy index…
Assumed by34
- CategoryTheory.Hom.addCommMonoid
- CategoryTheory.IsCommAddMonObj.add_comm
- CategoryTheory.IsCommAddMonObj.add_comm'
- CategoryTheory.AddGrp.Hom.hom_nsmul
- CategoryTheory.AddMonObj.add_add_add_comm'
- CategoryTheory.AddMonObj.add_add_add_comm
- CategoryTheory.AddMon.Hom.hom_nsmul
- CategoryTheory.AddMonObj.instIsAddMonHomAddOfIsCommAddMonObj
- CategoryTheory.instIsAddMonHomNegOfIsCommAddMonObj
- CategoryTheory.AddMon.hom_zero
- CategoryTheory.AddGrp.instAddGrpObj
- CategoryTheory.AddGrp.Hom.hom_hom_sub
- CategoryTheory.AddMonObj.add_add_add_comm'_assoc
- CategoryTheory.AddGrp.hom_add
- CategoryTheory.AddMon.Hom.hom_add
- CategoryTheory.AddGrp.hom_zero
- CategoryTheory.AddMon.instAddMonObjOfIsCommAddMonObjX
- CategoryTheory.AddGrp.instAddMonObj
- CategoryTheory.instIsAddMonHomNegHomOfIsCommAddMonObj
- CategoryTheory.AddGrp.Hom.hom_zero
- CategoryTheory.AddMonObj.add_add_add_comm_assoc
- CategoryTheory.AddMon.instIsCommAddMonObj
- CategoryTheory.AddGrp.Hom.hom_hom_zsmul
- CategoryTheory.AddGrpObj.addConj_eq_snd_of_isCommAddMonObj
- CategoryTheory.AddGrp.instIsCommAddMonObj
- CategoryTheory.AddMon.Hom.hom_zero
- CategoryTheory.IsAddMonHom.instNormalOfIsCommAddMonObjOfMono
- CategoryTheory.AddGrp.Hom.hom_hom_neg
- CategoryTheory.AddMon.hom_add
- CategoryTheory.instIsCommAddMonObjTensorObj
- CategoryTheory.IsCommAddMonObj.add_comm'_assoc
- CategoryTheory.AddGrp.instIsAddMonHom
- CategoryTheory.Hom.addCommGroup
- CategoryTheory.AddGrp.Hom.hom_add
Ancestors0
No ancestors.