mathlib3 documentation

algebra.order.monoid.type_tags

Ordered monoid structures on multiplicative α and additive α. #

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

@[protected, instance]
Equations
@[protected, instance]
def additive.has_le {α : Type u} [has_le α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def additive.has_lt {α : Type u} [has_lt α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def additive.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def additive.order_bot {α : Type u} [has_le α] [order_bot α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def additive.order_top {α : Type u} [has_le α] [order_top α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem additive.of_mul_le {α : Type u} [preorder α] {a b : α} :
@[simp]
theorem additive.of_mul_lt {α : Type u} [preorder α] {a b : α} :
@[simp]
@[simp]
theorem additive.to_mul_lt {α : Type u} [preorder α] {a b : additive α} :