Additional instances for ordered commutative groups.

instance OrderDual.orderedCommGroup {α : Type u_1} [OrderedCommGroup α] : OrderedCommGroup αᵒᵈ

Equations

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

instance OrderDual.orderedAddCommGroup {α : Type u_1} [OrderedAddCommGroup α] : OrderedAddCommGroup αᵒᵈ

Equations

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

instance OrderDual.linearOrderedCommGroup {α : Type u_1} [LinearOrderedCommGroup α] : LinearOrderedCommGroup αᵒᵈ

Equations

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

instance OrderDual.linearOrderedAddCommGroup {α : Type u_1} [LinearOrderedAddCommGroup α] : LinearOrderedAddCommGroup αᵒᵈ

Equations

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