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.

instance Positive.Subtype.inv {K : Type u_1} [LinearOrderedField K] : Inv { x // 0 < x }

@[simp]

theorem Positive.coe_inv {K : Type u_1} [LinearOrderedField K] (x : { x // 0 < x }) : ↑x⁻¹ = (↑x)⁻¹

instance Positive.instPowSubtypeLtToLTToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRingOfNatToOfNat0ToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToLinearOrderedSemifieldInt {K : Type u_1} [LinearOrderedField K] : Pow { x // 0 < x } ℤ

@[simp]

theorem Positive.coe_zpow {K : Type u_1} [LinearOrderedField K] (x : { x // 0 < x }) (n : ℤ) : ↑(x ^ n) = ↑x ^ n

instance Positive.instLinearOrderedCommGroupSubtypeLtToLTToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRingOfNatToOfNat0ToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToLinearOrderedSemifield {K : Type u_1} [LinearOrderedField K] : LinearOrderedCommGroup { x // 0 < x }