Mathlib Map

Structures · Algebra

AddMonoid

An AddMonoid is an AddSemigroup with an element 0 such that 0 + a = a + 0 = a.

Defined in
Mathlib.Algebra.Group.Defs
Shape
One type argument · adds zero_add, add_zero, nsmul_zero, nsmul_succ
Open in Mathlib docs

Extends3

Extended by6

Forgetful instances

Every AddMonoid is also a

Concrete types that are instances83

  • Int
  • Nat
  • Real
  • Rat
  • SeparationQuotient
  • ContinuousLinearMap
  • Filter.Germ
  • BoundedContinuousFunction
  • CStarMatrix
  • UniformSpace.Completion
  • TensorProduct
  • Unitization
  • WithConv
  • Matrix
  • HahnSeries
  • LocallyConstant
  • QuadraticAlgebra
  • MeasureTheory.SimpleFunc
  • EReal
  • MonoidAlgebra
  • RestrictedProduct
  • TrivSqZeroExt
  • AddMonoidAlgebra
  • DirectLimit
  • Finsupp
  • UniformFun
  • Zsqrtd
  • UniformOnFun
  • ZNum
  • SymAlg
  • DomAddAct
  • SkewMonoidAlgebra
  • AddUnits
  • ContMDiffMap
  • OreLocalization
  • ZeroAtInftyContinuousMap
  • CategoryTheory.Limits.Cone.pt
  • DFinsupp
  • WithCStarModule
  • MvPowerSeries
  • ArithmeticFunction
  • MeasureTheory.AEEqFun
  • RingCon.Quotient
  • Num
  • MulActionHom
  • ContinuousMultilinearMap
  • CompactlySupportedContinuousMap
  • Hamming
  • IncidenceAlgebra
  • DMatrix
  • ZeroHom
  • Function.locallyFinsuppWithin
  • ConvexBody
  • Seminorm
  • MultilinearMap
  • LinearPMap
  • AddCon.Quotient
  • Holor
  • ModuleCon.Quotient
  • OrderType
  • AddMonCat.carrier
  • AddMonoid.Coprod
  • AddOreLocalization
  • FormalGroup.Point
  • AddMonCat.FilteredColimits.M
  • PresentedAddMonoid
  • Subtype
  • Prod
  • OrderDual
  • Set.Elem
  • ULift
  • MulOpposite
  • Lex
  • AddOpposite
  • HasQuotient.Quotient
  • ContinuousMap
  • Shrink
  • WithTop
  • WithBot
  • Colex
  • Additive
  • WithZero
  • LinearMap

How is a type an instance?

Loading the hierarchy index…

Assumed by3,877

Ancestors14