Ordered group structures on Multiplicative α and Additive α.

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

Equations

• Multiplicative.orderedCommGroup = let __src := Multiplicative.commGroup; let __src_1 := Multiplicative.orderedCommMonoid; OrderedCommGroup.mk ⋯

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

Equations

• Additive.orderedAddCommGroup = let __src := Additive.addCommGroup; let __src_1 := Additive.orderedAddCommMonoid; OrderedAddCommGroup.mk ⋯

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.