Structures · Algebra
AddCommGroup
An additive commutative group is an additive group with commutative (+).
[Wikidata Q181296](https://www.wikidata.org/wiki/Q181296)
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds add_comm
Extends2
Extended by6
Forgetful instances
Every AddCommGroup is also a
Concrete types that are instances100
- Int
- Real
- Rat
- Quiver.Hom
- Complex
- SeparationQuotient
- CategoryTheory.Functor.obj
- ContinuousLinearMap
- Filter.Germ
- BoundedContinuousFunction
- Padic
- CStarMatrix
- UniformSpace.Completion
- TensorProduct
- Unitization
- WithConv
- Matrix
- HahnSeries
- LocallyConstant
- QuadraticAlgebra
- WithLp
- MeasureTheory.SimpleFunc
- FreeAbelianGroup
- MonoidAlgebra
- RestrictedProduct
- TrivSqZeroExt
- ModuleCat.carrier
- AddMonoidAlgebra
- DirectLimit
- Finsupp
- DirectSum
- UniformFun
- RestrictScalars
- Zsqrtd
- UniformOnFun
- ZNum
- SymAlg
- DomAddAct
- SkewMonoidAlgebra
- AddUnits
- ContinuousMapZero
- PerfectClosure
- ContMDiffMap
- OreLocalization
- PiTensorProduct
- QuaternionAlgebra
- ZeroAtInftyContinuousMap
- CategoryTheory.Limits.Cone.pt
- ContinuousAlternatingMap
- DFinsupp
- PreLp
- ContinuousLinearMapWOT
- LucasLehmer.X
- CategoryTheory.End
- WithCStarModule
- MvPowerSeries
- ArithmeticFunction
- AdicCompletion
- MeasureTheory.AEEqFun
- Representation.IntertwiningMap
- AdicCompletion.AdicCauchySequence
- RingCon.Quotient
- AddChar
- MulActionHom
- CentroidHom
- Poly
- ContinuousMultilinearMap
- CompactlySupportedContinuousMap
- SchwartzMap
- MeasureTheory.VectorMeasure
- AddMonoid.End
- Hamming
- AlternatingMap
- IncidenceAlgebra
- AddMonoidHom
- ContinuousAffineMap
- PolynomialModule
- DMatrix
- AddCommGroup.DirectLimit
- Module.DirectLimit
- NormedAddGroupHom
- ZeroHom
- TestFunction
- ContDiffMapSupportedIn
- KaehlerDifferential
- Algebra.Extension.H1Cotangent
- AlgebraicGeometry.Scheme.EllAdicCohomology
- UniformConvergenceCLM
- ContinuousAddMonoidHom
- PositiveLinearMap.PreGNS
- WeakDual
- Function.locallyFinsuppWithin
- Derivation
- AffineMap
- TangentSpace
- WeakSpace
- WeakBilin
- TopRep.V
- LieDerivation
- LeftInvariantDerivation
How is a type an instance?
Loading the hierarchy index…
Assumed by15,115
- FiniteDimensional
- deriv
- DifferentiableAt
- ModuleCat.of
- HasDerivAt
- DifferentiableWithinAt
- DifferentiableOn
- affineSpan
- fderiv
- Affine.Simplex.points
- fderivWithin
- HasFDerivWithinAt
- HasFDerivAt
- AffineSubspace.direction
- HasDerivWithinAt
- RootPairing.root
- CliffordAlgebra
- neg_smul
- Differentiable
- HasStrictFDerivAt
- derivWithin
- AffineMap.lineMap
- ArchimedeanClass
- Submodule.mkQ
- neg_neg_of_pos
- UniqueDiffOn
- ModuleCat.ofHom
- add_sub_cancel_left
- add_sub_cancel
- AddCircle
- LinearPMap.domain
- Wbtw
- HasStrictDerivAt
- AdicCompletion
- RootPairing.IsCrystallographic
- Finset.affineCombination
- LieSubmodule.toSubmodule
- slope
- AffineIndependent
- LieModule.toEnd
- CliffordAlgebra.ι
- RootPairing.Base.support
- DifferentiableAt.hasFDerivAt
- DifferentiableWithinAt.hasFDerivWithinAt
- ExteriorAlgebra
- LinearMap.det
- LinearPMap.toFun'
- RootPairing.coroot
- midpoint
- vectorSpan
Ancestors43
- Add
- AddAction
- AddCancelCommMonoid
- AddCancelMonoid
- AddCommMagma
- AddCommMonoid
- AddCommSemigroup
- AddGroup
- AddLeftCancelMonoid
- AddLeftCancelSemigroup
- AddMonoid
- AddRightCancelMonoid
- AddRightCancelSemigroup
- AddSemigroup
- AddSemigroupAction
- AddTorsor
- AddZero
- AddZeroClass
- HAdd
- HSub
- HVAdd
- InvolutiveNeg
- IsLeftCancelAdd
- IsRightCancelAdd
- Lean.Grind.AddCommGroup
- Lean.Grind.AddCommMonoid
- Lean.Grind.IntModule
- Lean.Grind.NatModule
- NSMul
- Neg
- NegZeroClass
- Nonempty
- OfNat
- One
- Sub
- SubNegMonoid
- SubNegZeroMonoid
- SubtractionCommMonoid
- SubtractionMonoid
- VAdd
- VSub
- ZSMul
- Zero