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.

ink

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

Equations

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

ink

@[simp]

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

ink

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

Equations

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

ink

@[simp]

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

ink

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

Equations

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