Ordered group structures on Multiplicative α and Additive α.

instance Multiplicative.orderedCommGroup {α : Type u_1} [OrderedAddCommGroup α] : OrderedCommGroup (Multiplicative α)

Equations

• Multiplicative.orderedCommGroup = OrderedCommGroup.mk ⋯

instance Additive.orderedAddCommGroup {α : Type u_1} [OrderedCommGroup α] : OrderedAddCommGroup (Additive α)

Equations

• Additive.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯

instance Multiplicative.linearOrderedCommGroup {α : Type u_1} [LinearOrderedAddCommGroup α] : LinearOrderedCommGroup (Multiplicative α)

Equations

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

instance Additive.linearOrderedAddCommGroup {α : Type u_1} [LinearOrderedCommGroup α] : LinearOrderedAddCommGroup (Additive α)

Equations

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