Mathlib Map

Structures · Algebra

CommMonoid

A commutative monoid is a monoid with commutative (*).

Defined in
Mathlib.Algebra.Group.Defs
Shape
One type argument · adds mul_comm
Open in Mathlib docs

Extends2

Extended by7

Concrete types that are instances68

  • Int
  • Nat
  • Real
  • Rat
  • SeparationQuotient
  • CategoryTheory.Functor.obj
  • Filter.Germ
  • BoundedContinuousFunction
  • UInt64
  • UInt8
  • UInt16
  • UInt32
  • Unitization
  • WithConv
  • NonemptyInterval
  • LocallyConstant
  • USize
  • DomMulAct
  • MeasureTheory.SimpleFunc
  • RestrictedProduct
  • TrivSqZeroExt
  • DirectLimit
  • UniformFun
  • Zsqrtd
  • UniformOnFun
  • Interval
  • PerfectClosure
  • ContMDiffMap
  • OreLocalization
  • CategoryTheory.Limits.Cone.pt
  • SetSemiring
  • PNat
  • Tropical
  • UpperSet
  • LowerSet
  • Cardinal
  • MeasureTheory.AEEqFun
  • RingCon.Quotient
  • AddChar
  • MulActionHom
  • Perfection
  • Associates
  • OneHom
  • CategoryTheory.Skeleton
  • MonCat.carrier
  • ContinuousMonoidHom
  • PosNum
  • GroupLike
  • Con.Quotient
  • HomogeneousLocalization.NumDenSameDeg
  • IterateMulAct
  • GradedMonoid
  • CommMonCat.carrier
  • Subtype
  • Prod
  • OrderDual
  • Set.Elem
  • ULift
  • MulOpposite
  • Fin
  • Lex
  • AddOpposite
  • ContinuousMap
  • Shrink
  • Colex
  • Multiplicative
  • MonoidHom
  • WithOne

How is a type an instance?

Loading the hierarchy index…

Assumed by2,429

Ancestors20