Structures · Algebra
AddCommMonoid
An additive commutative monoid is an additive monoid with commutative (+).
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds add_comm
Extends2
Extended by9
Forgetful instances
Every AddCommMonoid is also a
Concrete types that are instances100
- Int
- Nat
- Real
- Rat
- Quiver.Hom
- Complex
- SeparationQuotient
- CategoryTheory.Functor.obj
- ContinuousLinearMap
- ENNReal
- Filter.Germ
- BoundedContinuousFunction
- CStarMatrix
- TensorProduct
- Unitization
- WithConv
- Matrix
- HahnSeries
- NonemptyInterval
- LocallyConstant
- QuadraticAlgebra
- MeasureTheory.SimpleFunc
- EReal
- MonoidAlgebra
- RestrictedProduct
- TrivSqZeroExt
- AddMonoidAlgebra
- DirectLimit
- Finsupp
- DirectSum
- UniformFun
- RestrictScalars
- UniformOnFun
- SymAlg
- DomAddAct
- SkewMonoidAlgebra
- Interval
- ContinuousMapZero
- ContMDiffMap
- OreLocalization
- PiTensorProduct
- ZeroAtInftyContinuousMap
- CategoryTheory.Limits.Cone.pt
- ContinuousAlternatingMap
- DFinsupp
- SetSemiring
- Tropical
- MvPowerSeries
- ArithmeticFunction
- UpperSet
- LowerSet
- MeasureTheory.AEEqFun
- Representation.IntertwiningMap
- LieSubalgebra
- RingCon.Quotient
- LieSubmodule
- RingQuot
- AddChar
- MulActionHom
- Ring.DirectLimit
- CentroidHom
- FreeAlgebra
- ContinuousMultilinearMap
- CompactlySupportedContinuousMap
- MeasureTheory.Measure
- MeasureTheory.VectorMeasure
- AddMonoid.End
- Hamming
- AlternatingMap
- IncidenceAlgebra
- AddMonoidHom
- ArchimedeanClass
- DMatrix
- AddCommGroup.DirectLimit
- Module.DirectLimit
- ZeroHom
- ProbabilityTheory.Kernel
- ContinuousAddMonoidHom
- WeakDual
- Function.locallyFinsuppWithin
- Derivation
- MeasureTheory.OuterMeasure
- WeakSpace
- WeakBilin
- SemimoduleCat.carrier
- ConvexBody
- PrimeMultiset
- QuadraticMap
- Seminorm
- MultilinearMap
- PolynomialLaw
- LinearPMap
- MonomialOrder.syn
- HahnSeries.SummableFamily
- BoxIntegral.BoxAdditiveMap
- AddCon.Quotient
- Holor
- Representation.asModule
- FormalMultilinearSeries
- Module.AEval
How is a type an instance?
Loading the hierarchy index…
Assumed by21,744
- Finsupp.support_smul_eq
- AlternatingMap.curryLeft_compAlternatingMap
- AlternatingMap.curryLeft_compAlternatingMap
- AlternatingMap.curryLeft_compAlternatingMap
- Submodule.span_range_subtype_eq_top_iff
- DirectedSystem.rTensor
- DirectedSystem.rTensor
- DFinsupp.instPosSMulReflectLE
- Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff
- AddMonoidHom.coe_finset_sum
- StrictConvex
- AlternatingMap.congr_fun
- AlternatingMap.congr_fun
- Finsupp.comp_liftAddHom
- Finsupp.comp_liftAddHom
- LinearMap.extendScalarsOfSurjectiveEquiv.congr_simp
- LinearMap.extendScalarsOfSurjectiveEquiv.congr_simp
- Fintype.sum_eq_zero_iff_of_nonpos
- ContinuousAlternatingMap.coe_mk
- ContinuousAlternatingMap.coe_mk
- StrictConcaveOn.dual
- StrictConcaveOn.dual
- Basis.piTensorProduct_apply
- ProperCone.instCoePointedCone
- FormalMultilinearSeries.const_smul_sum_apply
- FormalMultilinearSeries.const_smul_sum_apply
- HahnSeries.order_mul_of_ne_zero
- Finset.subsetSum_mono
- Matrix.conjTranspose_inv_ofNat_smul
- QuasiconvexOn.convex_lt
- Topology.IsInducing.summable_iff_tsum_comp_mem_range
- Topology.IsInducing.summable_iff_tsum_comp_mem_range
- IsSymmetricAlgebra.comp_equiv
- HasSum.nat_add_neg_add_one
- LowerSemicontinuous.add'
- LinearMap.polar_mem_iff
- LinearMap.polar_mem_iff
- Submodule.restrictScalars_mem
- ContinuousAlternatingMap.compContinuousLinearMap
- ContinuousAlternatingMap.compContinuousLinearMap
- ContinuousAlternatingMap.compContinuousLinearMap
- MultilinearMap.currySum_smul
- MultilinearMap.currySum_smul
- Submodule.toBaseChange.toLinearEquiv_apply
- Representation.freeLiftLEquiv_symm_apply
- DirectSum.of_eq_of_ne
- SkewPolynomial
- Submodule.pOrder.congr_simp
- TensorProduct.lid
- SkewMonoidAlgebra.mapDomain_apply