Mathlib Map

Structures · Algebra

AddSemigroup

An additive semigroup is a type with an associative (+).

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

Extends1

Extended by4

Concrete types that are instances39

  • Int
  • Nat
  • Real
  • Rat
  • SeparationQuotient
  • Filter.Germ
  • CStarMatrix
  • TensorProduct
  • Unitization
  • Matrix
  • LocallyConstant
  • TrivSqZeroExt
  • DirectLimit
  • Zsqrtd
  • DomAddAct
  • ContMDiffMap
  • PEmpty
  • RingCon.Quotient
  • DMatrix
  • LinearPMap
  • AddCon.Quotient
  • Holor
  • ModuleCon.Quotient
  • FreeAddSemigroup
  • AddMagma.FreeAddSemigroup
  • AddSemigrp.carrier
  • Subtype
  • Prod
  • OrderDual
  • ULift
  • MulOpposite
  • Lex
  • AddOpposite
  • ContinuousMap
  • Shrink
  • WithTop
  • WithBot
  • Colex
  • Additive

How is a type an instance?

Loading the hierarchy index…

Assumed by199

Ancestors4