Mathlib Map

Structures · Algebra

IsOrderedAddMonoid

An ordered (additive) monoid is a monoid with a preorder such that addition is monotone.

Defined in
Mathlib.Algebra.Order.Monoid.Defs
Shape
One type argument · adds add_le_add_left, add_le_add_right
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by4

Concrete types that are instances34

  • Int
  • Nat
  • Real
  • Rat
  • ENNReal
  • Filter.Germ
  • BoundedContinuousFunction
  • MeasureTheory.SimpleFunc
  • EReal
  • Finsupp
  • Zsqrtd
  • ZNum
  • AddUnits
  • DFinsupp
  • LieSubalgebra
  • CompactlySupportedContinuousMap
  • MeasureTheory.Measure
  • ArchimedeanClass
  • Function.locallyFinsuppWithin
  • MeasureTheory.OuterMeasure
  • MonomialOrder.syn
  • Subtype
  • Prod
  • OrderDual
  • MulOpposite
  • Lex
  • AddOpposite
  • ContinuousMap
  • WithTop
  • WithBot
  • Colex
  • Additive
  • Submodule
  • LinearMap

How is a type an instance?

Loading the hierarchy index…

Assumed by1,845

Ancestors0

No ancestors.