Ordered monoid structures on the order dual.

instance OrderDual.orderedCommMonoid {α : Type u} [OrderedCommMonoid α] : OrderedCommMonoid αᵒᵈ

Equations

• OrderDual.orderedCommMonoid = { toCommMonoid := OrderDual.instCommMonoid, toPartialOrder := OrderDual.instPartialOrder α, mul_le_mul_left := ⋯ }

instance OrderDual.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] : OrderedAddCommMonoid αᵒᵈ

Equations

• OrderDual.orderedAddCommMonoid = { toAddCommMonoid := OrderDual.instAddCommMonoid, toPartialOrder := OrderDual.instPartialOrder α, add_le_add_left := ⋯ }

instance OrderDual.OrderedCancelCommMonoid.to_mulLeftReflectLE {α : Type u} [OrderedCancelCommMonoid α] : MulLeftReflectLE αᵒᵈ

instance OrderDual.OrderedCancelAddCommMonoid.to_mulLeftReflectLE {α : Type u} [OrderedCancelAddCommMonoid α] : AddLeftReflectLE αᵒᵈ

instance OrderDual.orderedCancelCommMonoid {α : Type u} [OrderedCancelCommMonoid α] : OrderedCancelCommMonoid αᵒᵈ

Equations

• OrderDual.orderedCancelCommMonoid = { toOrderedCommMonoid := OrderDual.orderedCommMonoid, le_of_mul_le_mul_left := ⋯ }

instance OrderDual.orderedAddCancelCommMonoid {α : Type u} [OrderedCancelAddCommMonoid α] : OrderedCancelAddCommMonoid αᵒᵈ

Equations

• OrderDual.orderedAddCancelCommMonoid = { toOrderedAddCommMonoid := OrderDual.orderedAddCommMonoid, le_of_add_le_add_left := ⋯ }

instance OrderDual.linearOrderedCancelCommMonoid {α : Type u} [LinearOrderedCancelCommMonoid α] : LinearOrderedCancelCommMonoid αᵒᵈ

Equations

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

instance OrderDual.linearOrderedAddCancelCommMonoid {α : Type u} [LinearOrderedCancelAddCommMonoid α] : LinearOrderedCancelAddCommMonoid αᵒᵈ

Equations

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

instance OrderDual.linearOrderedCommMonoid {α : Type u} [LinearOrderedCommMonoid α] : LinearOrderedCommMonoid αᵒᵈ

Equations

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

instance OrderDual.linearOrderedAddCommMonoid {α : Type u} [LinearOrderedAddCommMonoid α] : LinearOrderedAddCommMonoid αᵒᵈ

Equations

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