mathlib3 documentation

algebra.order.monoid.order_dual

Ordered monoid structures on the order dual. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def order_dual.contravariant_class_mul_le {α : Type u} [has_le α] [has_mul α] [c : contravariant_class α α has_mul.mul has_le.le] :
contravariant_class αᵒᵈ αᵒᵈ has_mul.mul has_le.le
source
@[protected, instance]
def order_dual.contravariant_class_add_le {α : Type u} [has_le α] [has_add α] [c : contravariant_class α α has_add.add has_le.le] :
contravariant_class αᵒᵈ αᵒᵈ has_add.add has_le.le
source
@[protected, instance]
def order_dual.covariant_class_mul_le {α : Type u} [has_le α] [has_mul α] [c : covariant_class α α has_mul.mul has_le.le] :
covariant_class αᵒᵈ αᵒᵈ has_mul.mul has_le.le
source
@[protected, instance]
def order_dual.covariant_class_add_le {α : Type u} [has_le α] [has_add α] [c : covariant_class α α has_add.add has_le.le] :
covariant_class αᵒᵈ αᵒᵈ has_add.add has_le.le
source
@[protected, instance]
def order_dual.contravariant_class_swap_add_le {α : Type u} [has_le α] [has_add α] [c : contravariant_class α α (function.swap has_add.add) has_le.le] :
contravariant_class αᵒᵈ αᵒᵈ (function.swap has_add.add) has_le.le
source
@[protected, instance]
def order_dual.contravariant_class_swap_mul_le {α : Type u} [has_le α] [has_mul α] [c : contravariant_class α α (function.swap has_mul.mul) has_le.le] :
contravariant_class αᵒᵈ αᵒᵈ (function.swap has_mul.mul) has_le.le
source
@[protected, instance]
def order_dual.covariant_class_swap_add_le {α : Type u} [has_le α] [has_add α] [c : covariant_class α α (function.swap has_add.add) has_le.le] :
covariant_class αᵒᵈ αᵒᵈ (function.swap has_add.add) has_le.le
source
@[protected, instance]
def order_dual.covariant_class_swap_mul_le {α : Type u} [has_le α] [has_mul α] [c : covariant_class α α (function.swap has_mul.mul) has_le.le] :
covariant_class αᵒᵈ αᵒᵈ (function.swap has_mul.mul) has_le.le
source
@[protected, instance]
def order_dual.contravariant_class_mul_lt {α : Type u} [has_lt α] [has_mul α] [c : contravariant_class α α has_mul.mul has_lt.lt] :
contravariant_class αᵒᵈ αᵒᵈ has_mul.mul has_lt.lt
source
@[protected, instance]
def order_dual.contravariant_class_add_lt {α : Type u} [has_lt α] [has_add α] [c : contravariant_class α α has_add.add has_lt.lt] :
contravariant_class αᵒᵈ αᵒᵈ has_add.add has_lt.lt
source
@[protected, instance]
def order_dual.covariant_class_add_lt {α : Type u} [has_lt α] [has_add α] [c : covariant_class α α has_add.add has_lt.lt] :
covariant_class αᵒᵈ αᵒᵈ has_add.add has_lt.lt
source
@[protected, instance]
def order_dual.covariant_class_mul_lt {α : Type u} [has_lt α] [has_mul α] [c : covariant_class α α has_mul.mul has_lt.lt] :
covariant_class αᵒᵈ αᵒᵈ has_mul.mul has_lt.lt
source
@[protected, instance]
def order_dual.contravariant_class_swap_mul_lt {α : Type u} [has_lt α] [has_mul α] [c : contravariant_class α α (function.swap has_mul.mul) has_lt.lt] :
contravariant_class αᵒᵈ αᵒᵈ (function.swap has_mul.mul) has_lt.lt
source
@[protected, instance]
def order_dual.contravariant_class_swap_add_lt {α : Type u} [has_lt α] [has_add α] [c : contravariant_class α α (function.swap has_add.add) has_lt.lt] :
contravariant_class αᵒᵈ αᵒᵈ (function.swap has_add.add) has_lt.lt
source
@[protected, instance]
def order_dual.covariant_class_swap_mul_lt {α : Type u} [has_lt α] [has_mul α] [c : covariant_class α α (function.swap has_mul.mul) has_lt.lt] :
covariant_class αᵒᵈ αᵒᵈ (function.swap has_mul.mul) has_lt.lt
source
@[protected, instance]
def order_dual.covariant_class_swap_add_lt {α : Type u} [has_lt α] [has_add α] [c : covariant_class α α (function.swap has_add.add) has_lt.lt] :
covariant_class αᵒᵈ αᵒᵈ (function.swap has_add.add) has_lt.lt
source
@[protected, instance]
def order_dual.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :
ordered_add_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.ordered_comm_monoid {α : Type u} [ordered_comm_monoid α] :
ordered_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.ordered_cancel_comm_monoid.to_contravariant_class {α : Type u} [ordered_cancel_comm_monoid α] :
contravariant_class αᵒᵈ αᵒᵈ has_mul.mul has_le.le
source
@[protected, instance]
def ordered_cancel_add_comm_monoid.to_contravariant_class {α : Type u} [ordered_cancel_add_comm_monoid α] :
contravariant_class αᵒᵈ αᵒᵈ has_add.add has_le.le
source
@[protected, instance]
def order_dual.ordered_cancel_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] :
ordered_cancel_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.ordered_cancel_add_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :
ordered_cancel_add_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.linear_ordered_cancel_comm_monoid {α : Type u} [linear_ordered_cancel_comm_monoid α] :
linear_ordered_cancel_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.linear_ordered_cancel_add_comm_monoid {α : Type u} [linear_ordered_cancel_add_comm_monoid α] :
linear_ordered_cancel_add_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.linear_ordered_add_comm_monoid {α : Type u} [linear_ordered_add_comm_monoid α] :
linear_ordered_add_comm_monoid αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.linear_ordered_comm_monoid {α : Type u} [linear_ordered_comm_monoid α] :
linear_ordered_comm_monoid αᵒᵈ
Equations