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.

@[implicit_reducible]

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

@[simp]

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

@[implicit_reducible]

instance Positive.instPowSubtypeLtOfNatInt_mathlib {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Pow { x : K // 0 < x } ℤ

@[simp]

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

@[implicit_reducible]

instance Positive.instCommGroupSubtypeLtOfNat {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : CommGroup { x : K // 0 < x }