Documentation

Mathlib.Algebra.Order.Monoid.TypeTags

Ordered monoid structures on Multiplicative α and Additive α. #

source
instance instForAllLEMultiplicative {α : Type u_1} [LE α] :
LE (Multiplicative α)
source
instance instForAllLEAdditive {α : Type u_1} [LE α] :
LE (Additive α)
source
instance instForAllLTMultiplicative {α : Type u_1} [LT α] :
LT (Multiplicative α)
source
instance instForAllLTAdditive {α : Type u_1} [LT α] :
LT (Additive α)
source
instance Multiplicative.preorder {α : Type u_1} [Preorder α] :
Preorder (Multiplicative α)
source
instance Additive.preorder {α : Type u_1} [Preorder α] :
Preorder (Additive α)
source
instance Multiplicative.partialOrder {α : Type u_1} [PartialOrder α] :
PartialOrder (Multiplicative α)
source
instance Additive.partialOrder {α : Type u_1} [PartialOrder α] :
PartialOrder (Additive α)
source
instance Multiplicative.linearOrder {α : Type u_1} [LinearOrder α] :
LinearOrder (Multiplicative α)
source
instance Additive.linearOrder {α : Type u_1} [LinearOrder α] :
LinearOrder (Additive α)
source
instance Multiplicative.orderBot {α : Type u_1} [LE α] [OrderBot α] :
OrderBot (Multiplicative α)
source
instance Additive.orderBot {α : Type u_1} [LE α] [OrderBot α] :
OrderBot (Additive α)
source
instance Multiplicative.orderTop {α : Type u_1} [LE α] [OrderTop α] :
OrderTop (Multiplicative α)
source
instance Additive.orderTop {α : Type u_1} [LE α] [OrderTop α] :
OrderTop (Additive α)
source
instance Multiplicative.boundedOrder {α : Type u_1} [LE α] [BoundedOrder α] :
BoundedOrder (Multiplicative α)
source
instance Additive.boundedOrder {α : Type u_1} [LE α] [BoundedOrder α] :
BoundedOrder (Additive α)
source
instance Multiplicative.orderedCommMonoid {α : Type u_1} [OrderedAddCommMonoid α] :
OrderedCommMonoid (Multiplicative α)
source
instance Additive.orderedAddCommMonoid {α : Type u_1} [OrderedCommMonoid α] :
OrderedAddCommMonoid (Additive α)
source
instance Multiplicative.orderedCancelAddCommMonoid {α : Type u_1} [OrderedCancelAddCommMonoid α] :
OrderedCancelCommMonoid (Multiplicative α)
source
instance Additive.orderedCancelAddCommMonoid {α : Type u_1} [OrderedCancelCommMonoid α] :
OrderedCancelAddCommMonoid (Additive α)
source
instance Multiplicative.linearOrderedCommMonoid {α : Type u_1} [LinearOrderedAddCommMonoid α] :
LinearOrderedCommMonoid (Multiplicative α)
source
instance Additive.linearOrderedAddCommMonoid {α : Type u_1} [LinearOrderedCommMonoid α] :
LinearOrderedAddCommMonoid (Additive α)
source
instance Multiplicative.existsMulOfLe {α : Type u_1} [Add α] [LE α] [ExistsAddOfLE α] :
ExistsMulOfLE (Multiplicative α)
source
instance Additive.existsAddOfLe {α : Type u_1} [Mul α] [LE α] [ExistsMulOfLE α] :
ExistsAddOfLE (Additive α)
source
instance Multiplicative.canonicallyOrderedMonoid {α : Type u_1} [CanonicallyOrderedAddMonoid α] :
CanonicallyOrderedMonoid (Multiplicative α)
source
instance Additive.canonicallyOrderedAddMonoid {α : Type u_1} [CanonicallyOrderedMonoid α] :
CanonicallyOrderedAddMonoid (Additive α)
source
instance Multiplicative.canonicallyLinearOrderedMonoid {α : Type u_1} [CanonicallyLinearOrderedAddMonoid α] :
CanonicallyLinearOrderedMonoid (Multiplicative α)
source
instance instCanonicallyLinearOrderedAddMonoidAdditive {α : Type u_1} [CanonicallyLinearOrderedMonoid α] :
CanonicallyLinearOrderedAddMonoid (Additive α)
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