Ordered group structures on Multiplicative α and Additive α.

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

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