Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags

Ordered monoid structures on Multiplicative α and Additive α. #

source
@[implicit_reducible]
instance instLEMultiplicative {α : Type u_1} [LE α] :
LE (Multiplicative α)
Equations
source
@[implicit_reducible]
instance instLEAdditive {α : Type u_1} [LE α] :
LE (Additive α)
Equations
source
@[implicit_reducible]
instance instLTMultiplicative {α : Type u_1} [LT α] :
LT (Multiplicative α)
Equations
source
@[implicit_reducible]
instance instLTAdditive {α : Type u_1} [LT α] :
LT (Additive α)
Equations
source
@[implicit_reducible]
instance Multiplicative.preorder {α : Type u_1} [Preorder α] :
Preorder (Multiplicative α)
Equations
source
@[implicit_reducible]
instance Additive.preorder {α : Type u_1} [Preorder α] :
Preorder (Additive α)
Equations
source
@[implicit_reducible]
instance Multiplicative.partialOrder {α : Type u_1} [PartialOrder α] :
PartialOrder (Multiplicative α)
Equations
source
@[implicit_reducible]
instance Additive.partialOrder {α : Type u_1} [PartialOrder α] :
PartialOrder (Additive α)
Equations
source
@[implicit_reducible]
instance Multiplicative.linearOrder {α : Type u_1} [LinearOrder α] :
LinearOrder (Multiplicative α)
Equations
source
@[implicit_reducible]
instance Additive.linearOrder {α : Type u_1} [LinearOrder α] :
LinearOrder (Additive α)
Equations
source
@[implicit_reducible]
instance Multiplicative.orderBot {α : Type u_1} [LE α] [OrderBot α] :
OrderBot (Multiplicative α)
Equations
source
@[implicit_reducible]
instance Additive.orderBot {α : Type u_1} [LE α] [OrderBot α] :
OrderBot (Additive α)
Equations
source
@[implicit_reducible]
instance Multiplicative.orderTop {α : Type u_1} [LE α] [OrderTop α] :
OrderTop (Multiplicative α)
Equations
source
@[implicit_reducible]
instance Additive.orderTop {α : Type u_1} [LE α] [OrderTop α] :
OrderTop (Additive α)
Equations
source
@[implicit_reducible]
instance Multiplicative.boundedOrder {α : Type u_1} [LE α] [BoundedOrder α] :
BoundedOrder (Multiplicative α)
Equations
source
@[implicit_reducible]
instance Additive.boundedOrder {α : Type u_1} [LE α] [BoundedOrder α] :
BoundedOrder (Additive α)
Equations
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
@[simp]
theorem Additive.ofMul_le {α : Type u_1} [Preorder α] {a b : α} :
ofMul a ≤ ofMul b ↔ a ≤ b
source
@[simp]
theorem Additive.ofMul_lt {α : Type u_1} [Preorder α] {a b : α} :
ofMul a < ofMul b ↔ a < b
source
@[simp]
theorem Additive.toMul_le {α : Type u_1} [Preorder α] {a b : Additive α} :
toMul a ≤ toMul b ↔ a ≤ b
source
@[simp]
theorem Additive.toMul_lt {α : Type u_1} [Preorder α] {a b : Additive α} :
toMul a < toMul b ↔ a < b
source
theorem Additive.toMul_mono {α : Type u_1} [Preorder α] {a b : Additive α} :
a ≤ b → toMul a ≤ toMul b

Alias of the reverse direction of Additive.toMul_le.

source
theorem Additive.ofMul_mono {α : Type u_1} [Preorder α] {a b : α} :
a ≤ b → ofMul a ≤ ofMul b

Alias of the reverse direction of Additive.ofMul_le.

source
theorem Additive.toMul_strictMono {α : Type u_1} [Preorder α] {a b : Additive α} :
a < b → toMul a < toMul b

Alias of the reverse direction of Additive.toMul_lt.

source
theorem Additive.ofMul_strictMono {α : Type u_1} [Preorder α] {a b : α} :
a < b → ofMul a < ofMul b

Alias of the reverse direction of Additive.ofMul_lt.

source
@[deprecated Additive.ofMul_strictMono (since := "2025-11-18")]
theorem Additive.foMul_strictMono {α : Type u_1} [Preorder α] {a b : α} :
a < b → ofMul a < ofMul b

Alias of Additive.ofMul_strictMono.

Alias of the reverse direction of Additive.ofMul_lt.

source
@[simp]
theorem Additive.ofMul_top {α : Type u_1} [LE α] [OrderTop α] :
ofMul ⊤ = ⊤
source
@[simp]
theorem Additive.toMul_top {α : Type u_1} [LE α] [OrderTop α] :
toMul ⊤ = ⊤
source
@[simp]
theorem Additive.ofMul_eq_top {α : Type u_1} [LE α] [OrderTop α] {a : α} :
ofMul a = ⊤ ↔ a = ⊤
source
@[simp]
theorem Additive.toMul_eq_top {α : Type u_1} [LE α] [OrderTop α] {a : Additive α} :
toMul a = ⊤ ↔ a = ⊤
source
@[simp]
theorem Additive.ofMul_bot {α : Type u_1} [LE α] [OrderBot α] :
ofMul ⊥ = ⊥
source
@[simp]
theorem Additive.toMul_bot {α : Type u_1} [LE α] [OrderBot α] :
toMul ⊥ = ⊥
source
@[simp]
theorem Additive.ofMul_eq_bot {α : Type u_1} [LE α] [OrderBot α] {a : α} :
ofMul a = ⊥ ↔ a = ⊥
source
@[simp]
theorem Additive.toMul_eq_bot {α : Type u_1} [LE α] [OrderBot α] {a : Additive α} :
toMul a = ⊥ ↔ a = ⊥
source
@[simp]
theorem Multiplicative.ofAdd_le {α : Type u_1} [Preorder α] {a b : α} :
ofAdd a ≤ ofAdd b ↔ a ≤ b
source
@[simp]
theorem Multiplicative.ofAdd_lt {α : Type u_1} [Preorder α] {a b : α} :
ofAdd a < ofAdd b ↔ a < b
source
@[simp]
theorem Multiplicative.toAdd_le {α : Type u_1} [Preorder α] {a b : Multiplicative α} :
toAdd a ≤ toAdd b ↔ a ≤ b
source
@[simp]
theorem Multiplicative.toAdd_lt {α : Type u_1} [Preorder α] {a b : Multiplicative α} :
toAdd a < toAdd b ↔ a < b
source
theorem Multiplicative.toAdd_mono {α : Type u_1} [Preorder α] {a b : Multiplicative α} :
a ≤ b → toAdd a ≤ toAdd b

Alias of the reverse direction of Multiplicative.toAdd_le.

source
theorem Multiplicative.ofAdd_mono {α : Type u_1} [Preorder α] {a b : α} :
a ≤ b → ofAdd a ≤ ofAdd b

Alias of the reverse direction of Multiplicative.ofAdd_le.

source
theorem Multiplicative.toAdd_strictMono {α : Type u_1} [Preorder α] {a b : Multiplicative α} :
a < b → toAdd a < toAdd b

Alias of the reverse direction of Multiplicative.toAdd_lt.

source
theorem Multiplicative.ofAdd_strictMono {α : Type u_1} [Preorder α] {a b : α} :
a < b → ofAdd a < ofAdd b

Alias of the reverse direction of Multiplicative.ofAdd_lt.

source
@[simp]
theorem Multiplicative.ofAdd_top {α : Type u_1} [LE α] [OrderTop α] :
ofAdd ⊤ = ⊤
source
@[simp]
theorem Multiplicative.toAdd_top {α : Type u_1} [LE α] [OrderTop α] :
toAdd ⊤ = ⊤
source
@[simp]
theorem Multiplicative.ofAdd_eq_top {α : Type u_1} [LE α] [OrderTop α] {a : α} :
ofAdd a = ⊤ ↔ a = ⊤
source
@[simp]
theorem Multiplicative.toAdd_eq_top {α : Type u_1} [LE α] [OrderTop α] {a : Multiplicative α} :
toAdd a = ⊤ ↔ a = ⊤
source
@[simp]
theorem Multiplicative.ofAdd_bot {α : Type u_1} [LE α] [OrderBot α] :
ofAdd ⊥ = ⊥
source
@[simp]
theorem Multiplicative.toAdd_bot {α : Type u_1} [LE α] [OrderBot α] :
toAdd ⊥ = ⊥
source
@[simp]
theorem Multiplicative.ofAdd_eq_bot {α : Type u_1} [LE α] [OrderBot α] {a : α} :
ofAdd a = ⊥ ↔ a = ⊥
source
@[simp]
theorem Multiplicative.toAdd_eq_bot {α : Type u_1} [LE α] [OrderBot α] {a : Multiplicative α} :
toAdd a = ⊥ ↔ a = ⊥