Documentation

Mathlib.Algebra.Order.Monoid.TypeTags

Ordered monoid structures on Multiplicative α and Additive α. #

instance instForAllLEAdditive {α : Type u_1} [LE α] :
instance instForAllLTAdditive {α : Type u_1} [LT α] :
instance Additive.preorder {α : Type u_1} [Preorder α] :
instance Additive.orderBot {α : Type u_1} [LE α] [OrderBot α] :
instance Additive.orderTop {α : Type u_1} [LE α] [OrderTop α] :
@[simp]
theorem Additive.ofMul_le {α : Type u_1} [Preorder α] {a : α} {b : α} :
Additive.ofMul a Additive.ofMul b a b
@[simp]
theorem Additive.ofMul_lt {α : Type u_1} [Preorder α] {a : α} {b : α} :
Additive.ofMul a < Additive.ofMul b a < b
@[simp]
theorem Additive.toMul_le {α : Type u_1} [Preorder α] {a : Additive α} {b : Additive α} :
Additive.toMul a Additive.toMul b a b
@[simp]
theorem Additive.toMul_lt {α : Type u_1} [Preorder α] {a : Additive α} {b : Additive α} :
Additive.toMul a < Additive.toMul b a < b
@[simp]
theorem Multiplicative.ofAdd_le {α : Type u_1} [Preorder α] {a : α} {b : α} :
Multiplicative.ofAdd a Multiplicative.ofAdd b a b
@[simp]
theorem Multiplicative.ofAdd_lt {α : Type u_1} [Preorder α] {a : α} {b : α} :
Multiplicative.ofAdd a < Multiplicative.ofAdd b a < b
@[simp]
theorem Multiplicative.toAdd_le {α : Type u_1} [Preorder α] {a : Multiplicative α} {b : Multiplicative α} :
Multiplicative.toAdd a Multiplicative.toAdd b a b
@[simp]
theorem Multiplicative.toAdd_lt {α : Type u_1} [Preorder α] {a : Multiplicative α} {b : Multiplicative α} :
Multiplicative.toAdd a < Multiplicative.toAdd b a < b