Mathlib Map

Structures · Algebra

IsOrderedCancelAddMonoid

An ordered cancellative additive monoid is an ordered additive monoid in which addition is cancellative and monotone.

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

Extends1

Extended by1

Concrete types that are instances20

  • Nat
  • Real
  • Filter.Germ
  • Finsupp
  • DFinsupp
  • Num
  • PrimeMultiset
  • Seminorm
  • AddLocalization
  • MonomialOrder.syn
  • DegLex
  • DivisibleHull
  • Subtype
  • Prod
  • OrderDual
  • PUnit
  • Lex
  • Colex
  • Additive
  • Multiset

How is a type an instance?

Loading the hierarchy index…

Assumed by439

Ancestors1