Documentation

Mathlib.Algebra.Order.Monoid.TypeTags

Ordered monoid structures on Multiplicative α and Additive α. #

instance instLEMultiplicative {α : Type u_1} [LE α] :
Equations
  • instLEMultiplicative = inst
instance instLEAdditive {α : Type u_1} [LE α] :
Equations
  • instLEAdditive = inst
instance instLTMultiplicative {α : Type u_1} [LT α] :
Equations
  • instLTMultiplicative = inst
instance instLTAdditive {α : Type u_1} [LT α] :
Equations
  • instLTAdditive = inst
Equations
  • Multiplicative.preorder = inst
instance Additive.preorder {α : Type u_1} [Preorder α] :
Equations
  • Additive.preorder = inst
Equations
  • Multiplicative.partialOrder = inst
Equations
  • Additive.partialOrder = inst
Equations
  • Multiplicative.linearOrder = inst
Equations
  • Additive.linearOrder = inst
instance Multiplicative.orderBot {α : Type u_1} [LE α] [OrderBot α] :
Equations
  • Multiplicative.orderBot = inst
instance Additive.orderBot {α : Type u_1} [LE α] [OrderBot α] :
Equations
  • Additive.orderBot = inst
instance Multiplicative.orderTop {α : Type u_1} [LE α] [OrderTop α] :
Equations
  • Multiplicative.orderTop = inst
instance Additive.orderTop {α : Type u_1} [LE α] [OrderTop α] :
Equations
  • Additive.orderTop = inst
Equations
  • Multiplicative.boundedOrder = inst
instance Additive.boundedOrder {α : Type u_1} [LE α] [BoundedOrder α] :
Equations
  • Additive.boundedOrder = inst
Equations
Equations
Equations
  • Multiplicative.linearOrderedCommMonoid = LinearOrderedCommMonoid.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT
Equations
  • Additive.linearOrderedAddCommMonoid = LinearOrderedAddCommMonoid.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT
Equations
  • =
instance Additive.existsAddOfLe {α : Type u_1} [Mul α] [LE α] [ExistsMulOfLE α] :
Equations
  • =
Equations
@[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