Documentation

Mathlib.Algebra.Order.Monoid.TypeTags

Ordered monoid structures on Multiplicative α and Additive α. #

source
instance instLEMultiplicative {α : Type u_1} [LE α] :
LE (Multiplicative α)
Equations
  • instLEMultiplicative = inst
source
instance instLEAdditive {α : Type u_1} [LE α] :
LE (Additive α)
Equations
  • instLEAdditive = inst
source
instance instLTMultiplicative {α : Type u_1} [LT α] :
LT (Multiplicative α)
Equations
  • instLTMultiplicative = inst
source
instance instLTAdditive {α : Type u_1} [LT α] :
LT (Additive α)
Equations
  • instLTAdditive = inst
source
instance Multiplicative.preorder {α : Type u_1} [Preorder α] :
Preorder (Multiplicative α)
Equations
  • Multiplicative.preorder = inst
source
instance Additive.preorder {α : Type u_1} [Preorder α] :
Preorder (Additive α)
Equations
  • Additive.preorder = inst
source
instance Multiplicative.partialOrder {α : Type u_1} [PartialOrder α] :
PartialOrder (Multiplicative α)
Equations
  • Multiplicative.partialOrder = inst
source
instance Additive.partialOrder {α : Type u_1} [PartialOrder α] :
PartialOrder (Additive α)
Equations
  • Additive.partialOrder = inst
source
instance Multiplicative.linearOrder {α : Type u_1} [LinearOrder α] :
LinearOrder (Multiplicative α)
Equations
  • Multiplicative.linearOrder = inst
source
instance Additive.linearOrder {α : Type u_1} [LinearOrder α] :
LinearOrder (Additive α)
Equations
  • Additive.linearOrder = inst
source
instance Multiplicative.orderBot {α : Type u_1} [LE α] [OrderBot α] :
OrderBot (Multiplicative α)
Equations
  • Multiplicative.orderBot = inst
source
instance Additive.orderBot {α : Type u_1} [LE α] [OrderBot α] :
OrderBot (Additive α)
Equations
  • Additive.orderBot = inst
source
instance Multiplicative.orderTop {α : Type u_1} [LE α] [OrderTop α] :
OrderTop (Multiplicative α)
Equations
  • Multiplicative.orderTop = inst
source
instance Additive.orderTop {α : Type u_1} [LE α] [OrderTop α] :
OrderTop (Additive α)
Equations
  • Additive.orderTop = inst
source
instance Multiplicative.boundedOrder {α : Type u_1} [LE α] [BoundedOrder α] :
BoundedOrder (Multiplicative α)
Equations
  • Multiplicative.boundedOrder = inst
source
instance Additive.boundedOrder {α : Type u_1} [LE α] [BoundedOrder α] :
BoundedOrder (Additive α)
Equations
  • Additive.boundedOrder = inst
source
instance Multiplicative.orderedCommMonoid {α : Type u_1} [OrderedAddCommMonoid α] :
OrderedCommMonoid (Multiplicative α)
Equations
source
instance Additive.orderedAddCommMonoid {α : Type u_1} [OrderedCommMonoid α] :
OrderedAddCommMonoid (Additive α)
Equations
source
instance Multiplicative.orderedCancelAddCommMonoid {α : Type u_1} [OrderedCancelAddCommMonoid α] :
OrderedCancelCommMonoid (Multiplicative α)
Equations
source
instance Additive.orderedCancelAddCommMonoid {α : Type u_1} [OrderedCancelCommMonoid α] :
OrderedCancelAddCommMonoid (Additive α)
Equations
source
instance Multiplicative.linearOrderedCommMonoid {α : Type u_1} [LinearOrderedAddCommMonoid α] :
LinearOrderedCommMonoid (Multiplicative α)
Equations
  • Multiplicative.linearOrderedCommMonoid = LinearOrderedCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
source
instance Additive.linearOrderedAddCommMonoid {α : Type u_1} [LinearOrderedCommMonoid α] :
LinearOrderedAddCommMonoid (Additive α)
Equations
  • Additive.linearOrderedAddCommMonoid = LinearOrderedAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
source
instance Multiplicative.existsMulOfLe {α : Type u_1} [Add α] [LE α] [ExistsAddOfLE α] :
ExistsMulOfLE (Multiplicative α)
Equations
  • ⋯ = ⋯
source
instance Additive.existsAddOfLe {α : Type u_1} [Mul α] [LE α] [ExistsMulOfLE α] :
ExistsAddOfLE (Additive α)
Equations
  • ⋯ = ⋯
source
instance Multiplicative.canonicallyOrderedCommMonoid {α : Type u_1} [CanonicallyOrderedAddCommMonoid α] :
CanonicallyOrderedCommMonoid (Multiplicative α)
Equations
source
instance Additive.canonicallyOrderedAddCommMonoid {α : Type u_1} [CanonicallyOrderedCommMonoid α] :
CanonicallyOrderedAddCommMonoid (Additive α)
Equations
source
instance Multiplicative.canonicallyLinearOrderedCommMonoid {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] :
CanonicallyLinearOrderedCommMonoid (Multiplicative α)
Equations
source
instance instCanonicallyLinearOrderedAddCommMonoidAdditiveOfCanonicallyLinearOrderedCommMonoid {α : Type u_1} [CanonicallyLinearOrderedCommMonoid α] :
CanonicallyLinearOrderedAddCommMonoid (Additive α)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem Additive.ofMul_le {α : Type u_1} [Preorder α] {a : α} {b : α} :
Additive.ofMul a ≤ Additive.ofMul b ↔ a ≤ b
source
@[simp]
theorem Additive.ofMul_lt {α : Type u_1} [Preorder α] {a : α} {b : α} :
Additive.ofMul a < Additive.ofMul b ↔ a < b
source
@[simp]
theorem Additive.toMul_le {α : Type u_1} [Preorder α] {a : Additive α} {b : Additive α} :
Additive.toMul a ≤ Additive.toMul b ↔ a ≤ b
source
@[simp]
theorem Additive.toMul_lt {α : Type u_1} [Preorder α] {a : Additive α} {b : Additive α} :
Additive.toMul a < Additive.toMul b ↔ a < b
source
@[simp]
theorem Multiplicative.ofAdd_le {α : Type u_1} [Preorder α] {a : α} {b : α} :
Multiplicative.ofAdd a ≤ Multiplicative.ofAdd b ↔ a ≤ b
source
@[simp]
theorem Multiplicative.ofAdd_lt {α : Type u_1} [Preorder α] {a : α} {b : α} :
Multiplicative.ofAdd a < Multiplicative.ofAdd b ↔ a < b
source
@[simp]
theorem Multiplicative.toAdd_le {α : Type u_1} [Preorder α] {a : Multiplicative α} {b : Multiplicative α} :
Multiplicative.toAdd a ≤ Multiplicative.toAdd b ↔ a ≤ b
source
@[simp]
theorem Multiplicative.toAdd_lt {α : Type u_1} [Preorder α] {a : Multiplicative α} {b : Multiplicative α} :
Multiplicative.toAdd a < Multiplicative.toAdd b ↔ a < b