Mathlib Map

Structures · Algebra

AddZeroClass

Typeclass for expressing that a type M with addition and a zero satisfies 0 + a = a and a + 0 = a for all a : M.

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

Extends1

Extended by1

Concrete types that are instances42

  • SeparationQuotient
  • Filter.Germ
  • BoundedContinuousFunction
  • CStarMatrix
  • TensorProduct
  • Unitization
  • Matrix
  • LocallyConstant
  • TrivSqZeroExt
  • DirectLimit
  • Finsupp
  • DomAddAct
  • Interval
  • AddUnits
  • ZeroAtInftyContinuousMap
  • DFinsupp
  • RingCon.Quotient
  • MulActionHom
  • CompactlySupportedContinuousMap
  • ConvexCone
  • LinearPMap
  • WeierstrassCurve.Affine.Point
  • ContIntertwiningMap
  • AddCon.Quotient
  • ModuleCon.Quotient
  • AddMonoid.Coprod
  • StieltjesFunction
  • AddMonCat.FilteredColimits.M
  • Subtype
  • Prod
  • OrderDual
  • ULift
  • MulOpposite
  • Lex
  • AddOpposite
  • ContinuousMap
  • Shrink
  • WithTop
  • WithBot
  • Colex
  • Additive
  • WithZero

How is a type an instance?

Loading the hierarchy index…

Assumed by1,578

Ancestors9