Documentation

Mathlib.Algebra.Order.Monoid.TypeTags

Ordered monoid structures on Multiplicative α and Additive α. #

source
instance instForAllLEMultiplicative {α : Type u_1} [LE α] :
LE (Multiplicative α)
Equations
  • instForAllLEMultiplicative = inst
source
instance instForAllLEAdditive {α : Type u_1} [LE α] :
LE (Additive α)
Equations
  • instForAllLEAdditive = inst
source
instance instForAllLTMultiplicative {α : Type u_1} [LT α] :
LT (Multiplicative α)
Equations
  • instForAllLTMultiplicative = inst
source
instance instForAllLTAdditive {α : Type u_1} [LT α] :
LT (Additive α)
Equations
  • instForAllLTAdditive = 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
  • Multiplicative.orderedCommMonoid = let __src := Multiplicative.partialOrder; let __src_1 := Multiplicative.commMonoid; OrderedCommMonoid.mk ⋯
source
instance Additive.orderedAddCommMonoid {α : Type u_1} [OrderedCommMonoid α] :
OrderedAddCommMonoid (Additive α)
Equations
  • Additive.orderedAddCommMonoid = let __src := Additive.partialOrder; let __src_1 := Additive.addCommMonoid; OrderedAddCommMonoid.mk ⋯
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
  • One or more equations did not get rendered due to their size.
source
instance Additive.linearOrderedAddCommMonoid {α : Type u_1} [LinearOrderedCommMonoid α] :
LinearOrderedAddCommMonoid (Additive α)
Equations
  • One or more equations did not get rendered due to their size.
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
  • Multiplicative.canonicallyOrderedCommMonoid = let __src := Multiplicative.orderedCommMonoid; let __src_1 := Multiplicative.orderBot; let __src_2 := ⋯; CanonicallyOrderedCommMonoid.mk ⋯ ⋯
source
instance Additive.canonicallyOrderedAddCommMonoid {α : Type u_1} [CanonicallyOrderedCommMonoid α] :
CanonicallyOrderedAddCommMonoid (Additive α)
Equations
  • Additive.canonicallyOrderedAddCommMonoid = let __src := Additive.orderedAddCommMonoid; let __src_1 := Additive.orderBot; let __src_2 := ⋯; CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯
source
instance Multiplicative.canonicallyLinearOrderedCommMonoid {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] :
CanonicallyLinearOrderedCommMonoid (Multiplicative α)
Equations
  • One or more equations did not get rendered due to their size.
source
instance instCanonicallyLinearOrderedAddCommMonoidAdditive {α : 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