Mathlib Map

Structures · Algebra

AddGroup

An AddGroup is an AddMonoid with a unary - satisfying -a + a = 0. There is also a binary operation - such that a - b = a + -b, with a default so that a - b = a + -b holds by definition. Use AddGroup.ofLeftAxioms or AddGroup.ofRightAxioms to define an additive group structure on a type with the minimum proof obligations. [Wikidata Q83478](https://www.wikidata.org/wiki/Q83478)

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

Extends1

Extended by4

Forgetful instances

Every AddGroup is also a

Concrete types that are instances67

  • Int
  • Real
  • Rat
  • TopCat.carrier
  • SeparationQuotient
  • CategoryTheory.Functor.obj
  • Filter.Germ
  • CStarMatrix
  • UniformSpace.Completion
  • Unitization
  • WithConv
  • Matrix
  • HahnSeries
  • LocallyConstant
  • QuadraticAlgebra
  • MeasureTheory.SimpleFunc
  • RestrictedProduct
  • TrivSqZeroExt
  • DirectLimit
  • Finsupp
  • UniformFun
  • UniformOnFun
  • SymAlg
  • DomAddAct
  • SkewMonoidAlgebra
  • AddUnits
  • ContMDiffMap
  • OreLocalization
  • ZeroAtInftyContinuousMap
  • CategoryTheory.Limits.Cone.pt
  • DFinsupp
  • CauSeq
  • MvPowerSeries
  • ArithmeticFunction
  • MeasureTheory.AEEqFun
  • RingCon.Quotient
  • MulActionHom
  • CommRingCat.Colimits.ColimitType
  • CompactlySupportedContinuousMap
  • FreeAddGroup
  • Hamming
  • IncidenceAlgebra
  • RingCat.Colimits.ColimitType
  • DMatrix
  • ZeroHom
  • Function.locallyFinsuppWithin
  • AddGrpCat.carrier
  • FreeLieAlgebra
  • AddCon.Quotient
  • Holor
  • ModuleCon.Quotient
  • AddMonCat.carrier
  • AddAut
  • AddMonoid.Coprod
  • Subtype
  • Prod
  • OrderDual
  • Set.Elem
  • ULift
  • MulOpposite
  • Lex
  • AddOpposite
  • HasQuotient.Quotient
  • ContinuousMap
  • Shrink
  • Colex
  • Additive

How is a type an instance?

Loading the hierarchy index…

Assumed by5,260

Ancestors33