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.
@[simp]
instance
Positive.instPowSubtypeLtToLTToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRingOfNatToOfNat0ToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToLinearOrderedSemifieldInt
{K : Type u_1}
[inst : LinearOrderedField K]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Positive.coe_zpow
{K : Type u_1}
[inst : LinearOrderedField K]
(x : { x // 0 < x })
(n : ℤ)
:
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.