mathlib3 documentation

algebra.order.monoid.cancel.defs

Ordered cancellative monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[class]
structure ordered_cancel_add_comm_monoid (α : Type u) :

An ordered cancellative additive commutative monoid is an additive commutative monoid with a partial order, in which addition is cancellative and monotone.

Instances of this typeclass
Instances of other typeclasses for ordered_cancel_add_comm_monoid
  • ordered_cancel_add_comm_monoid.has_sizeof_inst
@[class]
structure ordered_cancel_comm_monoid (α : Type u) :

An ordered cancellative commutative monoid is a commutative monoid with a partial order, in which multiplication is cancellative and monotone.

Instances of this typeclass
Instances of other typeclasses for ordered_cancel_comm_monoid
  • ordered_cancel_comm_monoid.has_sizeof_inst
@[class]

A linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and monotone.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_cancel_add_comm_monoid
  • linear_ordered_cancel_add_comm_monoid.has_sizeof_inst
@[class]
structure linear_ordered_cancel_comm_monoid (α : Type u) :

A linearly ordered cancellative commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_cancel_comm_monoid
  • linear_ordered_cancel_comm_monoid.has_sizeof_inst