Ordered group structures on Multiplicative α and Additive α.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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