Algebraic structures on the set of positive numbers #
In this file we prove that the set of positive elements of a linear ordered field is a linear ordered commutative group.
@[simp]
@[simp]
instance
Positive.instLinearOrderedCommGroupSubtypeLtToLTToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRingOfNatToOfNat0ToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToLinearOrderedSemifield
{K : Type u_1}
[LinearOrderedField K]
:
LinearOrderedCommGroup { x // 0 < x }