# Documentation

Mathlib.Algebra.Order.Monoid.TypeTags

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

instance instForAllLEMultiplicative {α : Type u_1} [inst : LE α] :
LE ()
Equations
• instForAllLEMultiplicative = inst
instance instForAllLEAdditive {α : Type u_1} [inst : LE α] :
LE ()
Equations
instance instForAllLTMultiplicative {α : Type u_1} [inst : LT α] :
LT ()
Equations
• instForAllLTMultiplicative = inst
instance instForAllLTAdditive {α : Type u_1} [inst : LT α] :
LT ()
Equations
instance Multiplicative.preorder {α : Type u_1} [inst : ] :
Equations
• Multiplicative.preorder = inst
instance Additive.preorder {α : Type u_1} [inst : ] :
Equations
instance Multiplicative.partialOrder {α : Type u_1} [inst : ] :
Equations
• Multiplicative.partialOrder = inst
instance Additive.partialOrder {α : Type u_1} [inst : ] :
Equations
instance Multiplicative.linearOrder {α : Type u_1} [inst : ] :
Equations
• Multiplicative.linearOrder = inst
instance Additive.linearOrder {α : Type u_1} [inst : ] :
Equations
instance Multiplicative.orderBot {α : Type u_1} [inst : LE α] [inst : ] :
Equations
• Multiplicative.orderBot = inst
instance Additive.orderBot {α : Type u_1} [inst : LE α] [inst : ] :
Equations
instance Multiplicative.orderTop {α : Type u_1} [inst : LE α] [inst : ] :
Equations
• Multiplicative.orderTop = inst
instance Additive.orderTop {α : Type u_1} [inst : LE α] [inst : ] :
Equations
instance Multiplicative.boundedOrder {α : Type u_1} [inst : LE α] [inst : ] :
Equations
• Multiplicative.boundedOrder = inst
instance Additive.boundedOrder {α : Type u_1} [inst : LE α] [inst : ] :
Equations
instance Multiplicative.orderedCommMonoid {α : Type u_1} [inst : ] :
Equations
• Multiplicative.orderedCommMonoid = let src := Multiplicative.partialOrder; let src_1 := Multiplicative.commMonoid; OrderedCommMonoid.mk (_ : ∀ (a b : α), a b∀ (c : α), c + a c + b)
Equations
instance Multiplicative.orderedCancelAddCommMonoid {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
instance Multiplicative.linearOrderedCommMonoid {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
instance Multiplicative.existsMulOfLe {α : Type u_1} [inst : Add α] [inst : LE α] [inst : ] :
Equations
instance Additive.existsAddOfLe {α : Type u_1} [inst : Mul α] [inst : LE α] [inst : ] :
Equations
instance Multiplicative.canonicallyOrderedMonoid {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
instance Multiplicative.canonicallyLinearOrderedMonoid {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Additive.ofMul_le {α : Type u_1} [inst : ] {a : α} {b : α} :
@[simp]
theorem Additive.ofMul_lt {α : Type u_1} [inst : ] {a : α} {b : α} :
@[simp]
theorem Additive.toMul_le {α : Type u_1} [inst : ] {a : } {b : } :
@[simp]
theorem Additive.toMul_lt {α : Type u_1} [inst : ] {a : } {b : } :