Ordered group structures on Multiplicative α
and Additive α
. #
Equations
- Multiplicative.orderedCommGroup = let __src := Multiplicative.commGroup; let __src_1 := Multiplicative.orderedCommMonoid; OrderedCommGroup.mk ⋯
Equations
- Additive.orderedAddCommGroup = let __src := Additive.addCommGroup; let __src_1 := Additive.orderedAddCommMonoid; OrderedAddCommGroup.mk ⋯
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.