Additional instances for ordered commutative groups.

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

Equations

• OrderDual.orderedCommGroup = OrderedCommGroup.mk ⋯

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

Equations

• OrderDual.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯

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

Equations

• OrderDual.linearOrderedCommGroup = LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

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

Equations

• OrderDual.linearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯