Ordered monoid structures on Multiplicative α and Additive α.

@[instance_reducible]

instance instLEMultiplicative {α : Type u_1} [LE α] : LE (Multiplicative α)

Equations

• instLEMultiplicative = instLEMultiplicative._aux_1

@[instance_reducible]

instance instLEAdditive {α : Type u_1} [LE α] : LE (Additive α)

Equations

• instLEAdditive = instLEAdditive._aux_1

@[instance_reducible]

instance instLTMultiplicative {α : Type u_1} [LT α] : LT (Multiplicative α)

Equations

• instLTMultiplicative = instLTMultiplicative._aux_1

@[instance_reducible]

instance instLTAdditive {α : Type u_1} [LT α] : LT (Additive α)

Equations

• instLTAdditive = instLTAdditive._aux_1

@[instance_reducible]

instance Multiplicative.preorder {α : Type u_1} [Preorder α] : Preorder (Multiplicative α)

Equations

• Multiplicative.preorder = { toLE := instLEMultiplicative, toLT := instLTMultiplicative, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[instance_reducible]

instance Additive.preorder {α : Type u_1} [Preorder α] : Preorder (Additive α)

Equations

• Additive.preorder = { toLE := instLEAdditive, toLT := instLTAdditive, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[instance_reducible]

instance Multiplicative.partialOrder {α : Type u_1} [PartialOrder α] : PartialOrder (Multiplicative α)

Equations

• Multiplicative.partialOrder = { toPreorder := Multiplicative.preorder, le_antisymm := ⋯ }

@[instance_reducible]

instance Additive.partialOrder {α : Type u_1} [PartialOrder α] : PartialOrder (Additive α)

Equations

• Additive.partialOrder = { toPreorder := Additive.preorder, le_antisymm := ⋯ }

@[instance_reducible]

instance Multiplicative.linearOrder {α : Type u_1} [LinearOrder α] : LinearOrder (Multiplicative α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Additive.linearOrder {α : Type u_1} [LinearOrder α] : LinearOrder (Additive α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Multiplicative.orderBot {α : Type u_1} [LE α] [OrderBot α] : OrderBot (Multiplicative α)

Equations

• Multiplicative.orderBot = { toBot := Multiplicative.orderBot._aux_1, bot_le := ⋯ }

@[instance_reducible]

instance Additive.orderBot {α : Type u_1} [LE α] [OrderBot α] : OrderBot (Additive α)

Equations

• Additive.orderBot = { toBot := Additive.orderBot._aux_1, bot_le := ⋯ }

@[instance_reducible]

instance Multiplicative.orderTop {α : Type u_1} [LE α] [OrderTop α] : OrderTop (Multiplicative α)

Equations

• Multiplicative.orderTop = { toTop := Multiplicative.orderTop._aux_1, le_top := ⋯ }

@[instance_reducible]

instance Additive.orderTop {α : Type u_1} [LE α] [OrderTop α] : OrderTop (Additive α)

Equations

• Additive.orderTop = { toTop := Additive.orderTop._aux_1, le_top := ⋯ }

@[instance_reducible]

instance Multiplicative.boundedOrder {α : Type u_1} [LE α] [BoundedOrder α] : BoundedOrder (Multiplicative α)

Equations

• Multiplicative.boundedOrder = { toOrderTop := Multiplicative.orderTop, toOrderBot := Multiplicative.orderBot }

@[instance_reducible]

instance Additive.boundedOrder {α : Type u_1} [LE α] [BoundedOrder α] : BoundedOrder (Additive α)

Equations

• Additive.boundedOrder = { toOrderTop := Additive.orderTop, toOrderBot := Additive.orderBot }

instance Multiplicative.existsMulOfLe {α : Type u_1} [Add α] [LE α] [ExistsAddOfLE α] : ExistsMulOfLE (Multiplicative α)

instance Additive.existsAddOfLe {α : Type u_1} [Mul α] [LE α] [ExistsMulOfLE α] : ExistsAddOfLE (Additive α)

@[simp]

theorem Additive.ofMul_le {α : Type u_1} [Preorder α] {a b : α} : ofMul a ≤ ofMul b ↔ a ≤ b

@[simp]

theorem Additive.ofMul_lt {α : Type u_1} [Preorder α] {a b : α} : ofMul a < ofMul b ↔ a < b

@[simp]

theorem Additive.toMul_le {α : Type u_1} [Preorder α] {a b : Additive α} : toMul a ≤ toMul b ↔ a ≤ b

@[simp]

theorem Additive.toMul_lt {α : Type u_1} [Preorder α] {a b : Additive α} : toMul a < toMul b ↔ a < b

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.

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.

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.

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.

@[simp]

theorem Additive.ofMul_top {α : Type u_1} [LE α] [OrderTop α] : ofMul ⊤ = ⊤

@[simp]

theorem Additive.toMul_top {α : Type u_1} [LE α] [OrderTop α] : toMul ⊤ = ⊤

@[simp]

theorem Additive.ofMul_eq_top {α : Type u_1} [LE α] [OrderTop α] {a : α} : ofMul a = ⊤ ↔ a = ⊤

@[simp]

theorem Additive.toMul_eq_top {α : Type u_1} [LE α] [OrderTop α] {a : Additive α} : toMul a = ⊤ ↔ a = ⊤

@[simp]

theorem Additive.ofMul_bot {α : Type u_1} [LE α] [OrderBot α] : ofMul ⊥ = ⊥

@[simp]

theorem Additive.toMul_bot {α : Type u_1} [LE α] [OrderBot α] : toMul ⊥ = ⊥

@[simp]

theorem Additive.ofMul_eq_bot {α : Type u_1} [LE α] [OrderBot α] {a : α} : ofMul a = ⊥ ↔ a = ⊥

@[simp]

theorem Additive.toMul_eq_bot {α : Type u_1} [LE α] [OrderBot α] {a : Additive α} : toMul a = ⊥ ↔ a = ⊥

@[simp]

theorem Multiplicative.ofAdd_le {α : Type u_1} [Preorder α] {a b : α} : ofAdd a ≤ ofAdd b ↔ a ≤ b

@[simp]

theorem Multiplicative.ofAdd_lt {α : Type u_1} [Preorder α] {a b : α} : ofAdd a < ofAdd b ↔ a < b

@[simp]

theorem Multiplicative.toAdd_le {α : Type u_1} [Preorder α] {a b : Multiplicative α} : toAdd a ≤ toAdd b ↔ a ≤ b

@[simp]

theorem Multiplicative.toAdd_lt {α : Type u_1} [Preorder α] {a b : Multiplicative α} : toAdd a < toAdd b ↔ a < b

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.

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.

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.

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.

@[simp]

theorem Multiplicative.ofAdd_top {α : Type u_1} [LE α] [OrderTop α] : ofAdd ⊤ = ⊤

@[simp]

theorem Multiplicative.toAdd_top {α : Type u_1} [LE α] [OrderTop α] : toAdd ⊤ = ⊤

@[simp]

theorem Multiplicative.ofAdd_eq_top {α : Type u_1} [LE α] [OrderTop α] {a : α} : ofAdd a = ⊤ ↔ a = ⊤

@[simp]

theorem Multiplicative.toAdd_eq_top {α : Type u_1} [LE α] [OrderTop α] {a : Multiplicative α} : toAdd a = ⊤ ↔ a = ⊤

@[simp]

theorem Multiplicative.ofAdd_bot {α : Type u_1} [LE α] [OrderBot α] : ofAdd ⊥ = ⊥

@[simp]

theorem Multiplicative.toAdd_bot {α : Type u_1} [LE α] [OrderBot α] : toAdd ⊥ = ⊥

@[simp]

theorem Multiplicative.ofAdd_eq_bot {α : Type u_1} [LE α] [OrderBot α] {a : α} : ofAdd a = ⊥ ↔ a = ⊥

@[simp]

theorem Multiplicative.toAdd_eq_bot {α : Type u_1} [LE α] [OrderBot α] {a : Multiplicative α} : toAdd a = ⊥ ↔ a = ⊥