# Documentation

Mathlib.Algebra.Order.Monoid.TypeTags

# Ordered monoid structures on Multiplicative α and Additive α. #

instance instForAllLEMultiplicative {α : Type u_1} [LE α] :
LE ()
instance instForAllLEAdditive {α : Type u_1} [LE α] :
LE ()
instance instForAllLTMultiplicative {α : Type u_1} [LT α] :
LT ()
instance instForAllLTAdditive {α : Type u_1} [LT α] :
LT ()
instance Multiplicative.preorder {α : Type u_1} [] :
instance Additive.preorder {α : Type u_1} [] :
instance Multiplicative.partialOrder {α : Type u_1} [] :
instance Additive.partialOrder {α : Type u_1} [] :
instance Multiplicative.linearOrder {α : Type u_1} [] :
instance Additive.linearOrder {α : Type u_1} [] :
instance Multiplicative.orderBot {α : Type u_1} [LE α] [] :
instance Additive.orderBot {α : Type u_1} [LE α] [] :
instance Multiplicative.orderTop {α : Type u_1} [LE α] [] :
instance Additive.orderTop {α : Type u_1} [LE α] [] :
instance Multiplicative.boundedOrder {α : Type u_1} [LE α] [] :
instance Additive.boundedOrder {α : Type u_1} [LE α] [] :
instance Multiplicative.existsMulOfLe {α : Type u_1} [Add α] [LE α] [] :
instance Additive.existsAddOfLe {α : Type u_1} [Mul α] [LE α] [] :
@[simp]
theorem Additive.ofMul_le {α : Type u_1} [] {a : α} {b : α} :
@[simp]
theorem Additive.ofMul_lt {α : Type u_1} [] {a : α} {b : α} :
@[simp]
theorem Additive.toMul_le {α : Type u_1} [] {a : } {b : } :
@[simp]
theorem Additive.toMul_lt {α : Type u_1} [] {a : } {b : } :