HepLean Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual

Unbundled ordered monoid structures on the order dual. #

source
instance OrderDual.addLeftReflectLE {α : Type u} [LE α] [Add α] [c : AddLeftReflectLE α] :
AddLeftReflectLE αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.mulLeftReflectLE {α : Type u} [LE α] [Mul α] [c : MulLeftReflectLE α] :
MulLeftReflectLE αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.addLeftMono {α : Type u} [LE α] [Add α] [c : AddLeftMono α] :
AddLeftMono αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.mulLeftMono {α : Type u} [LE α] [Mul α] [c : MulLeftMono α] :
MulLeftMono αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.addRightReflectLE {α : Type u} [LE α] [Add α] [c : AddRightReflectLE α] :
AddRightReflectLE αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.mulRightReflectLE {α : Type u} [LE α] [Mul α] [c : MulRightReflectLE α] :
MulRightReflectLE αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.addRightMono {α : Type u} [LE α] [Add α] [c : AddRightMono α] :
AddRightMono αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.mulRightMono {α : Type u} [LE α] [Mul α] [c : MulRightMono α] :
MulRightMono αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.addLeftReflectLT {α : Type u} [LT α] [Add α] [c : AddLeftReflectLT α] :
AddLeftReflectLT αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.mulLeftReflectLT {α : Type u} [LT α] [Mul α] [c : MulLeftReflectLT α] :
MulLeftReflectLT αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.addLeftStrictMono {α : Type u} [LT α] [Add α] [c : AddLeftStrictMono α] :
AddLeftStrictMono αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.mulLeftStrictMono {α : Type u} [LT α] [Mul α] [c : MulLeftStrictMono α] :
MulLeftStrictMono αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.addRightReflectLT {α : Type u} [LT α] [Add α] [c : AddRightReflectLT α] :
AddRightReflectLT αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.mulRightReflectLT {α : Type u} [LT α] [Mul α] [c : MulRightReflectLT α] :
MulRightReflectLT αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.addRightStrictMono {α : Type u} [LT α] [Add α] [c : AddRightStrictMono α] :
AddRightStrictMono αᵒᵈ
Equations
  • ⋯ = ⋯
source
instance OrderDual.mulRightStrictMono {α : Type u} [LT α] [Mul α] [c : MulRightStrictMono α] :
MulRightStrictMono αᵒᵈ
Equations
  • ⋯ = ⋯