Documentation

Mathlib.Algebra.Order.Positive.Field

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 }) => (↑x)⁻¹, }
@[simp]
theorem Positive.coe_inv {K : Type u_1} [LinearOrderedField K] (x : { x : K // 0 < x }) :
x⁻¹ = (↑x)⁻¹
Equations
  • Positive.instPowSubtypeLtOfNatInt_mathlib = { pow := fun (x : { x : K // 0 < x }) (n : ) => x ^ n, }
@[simp]
theorem Positive.coe_zpow {K : Type u_1} [LinearOrderedField K] (x : { x : K // 0 < x }) (n : ) :
(x ^ n) = x ^ n
Equations
  • One or more equations did not get rendered due to their size.