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} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Inv { x : K // 0 < x }

Equations

• Positive.Subtype.inv = { inv := fun (x : { x : K // 0 < x }) => ⟨(↑x)⁻¹, ⋯⟩ }

@[simp]

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

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

Equations

• Positive.instPowSubtypeLtOfNatInt_mathlib = { pow := fun (x : { x : K // 0 < x }) (n : ℤ) => ⟨↑x ^ n, ⋯⟩ }

@[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

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

Equations

• One or more equations did not get rendered due to their size.