mathlib3 documentation

algebra.order.monoid.defs

Ordered monoids #

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

This file provides the definitions of ordered monoids.

@[instance]
@[class]
structure ordered_comm_monoid (α : Type u_2) :
Type u_2

An ordered commutative monoid is a commutative monoid with a partial order such that a ≤ b → c * a ≤ c * b (multiplication is monotone)

Instances of this typeclass
Instances of other typeclasses for ordered_comm_monoid
  • ordered_comm_monoid.has_sizeof_inst
@[class]
structure ordered_add_comm_monoid (α : Type u_2) :
Type u_2

An ordered (additive) commutative monoid is a commutative monoid with a partial order such that a ≤ b → c + a ≤ c + b (addition is monotone)

Instances of this typeclass
Instances of other typeclasses for ordered_add_comm_monoid
  • ordered_add_comm_monoid.has_sizeof_inst
theorem bit0_pos {α : Type u} [ordered_add_comm_monoid α] {a : α} (h : 0 < a) :
0 < bit0 a
@[class]
structure linear_ordered_add_comm_monoid (α : Type u_2) :
Type u_2

A linearly ordered additive commutative monoid.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_add_comm_monoid
  • linear_ordered_add_comm_monoid.has_sizeof_inst
@[class]
structure linear_ordered_comm_monoid (α : Type u_2) :
Type u_2

A linearly ordered commutative monoid.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_comm_monoid
  • linear_ordered_comm_monoid.has_sizeof_inst
@[class]
structure linear_ordered_add_comm_monoid_with_top (α : Type u_2) :
Type u_2

A linearly ordered commutative monoid with an additively absorbing element. Instances should include number systems with an infinite element adjoined.`

Instances of this typeclass
Instances of other typeclasses for linear_ordered_add_comm_monoid_with_top
  • linear_ordered_add_comm_monoid_with_top.has_sizeof_inst
@[simp]
theorem top_add {α : Type u} [linear_ordered_add_comm_monoid_with_top α] (a : α) :
@[simp]
theorem add_top {α : Type u} [linear_ordered_add_comm_monoid_with_top α] (a : α) :