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 : K // 0 < x }

Equations

• Positive.Subtype.inv = { inv := fun (x : { x : K // 0 < x }) => { val := (↑x)⁻¹, property := (_ : 0 < (↑x)⁻¹) } }

@[simp]

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

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

Equations

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

@[simp]

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

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

Equations

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