Ordered group structures on Multiplicative α
and Additive α
. #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
instance
Multiplicative.linearOrderedCommGroup
{α : Type u_1}
[inst : LinearOrderedAddCommGroup α]
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.