mathlib documentation

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.

@[protected, instance]
def positive.subtype.has_inv {K : Type u_1} [linear_ordered_field K] :
has_inv {x // 0 < x}
Equations
@[simp]
theorem positive.coe_inv {K : Type u_1} [linear_ordered_field K] (x : {x // 0 < x}) :
@[protected, instance]
def positive.int.has_pow {K : Type u_1} [linear_ordered_field K] :
has_pow {x // 0 < x}
Equations
@[simp]
theorem positive.coe_zpow {K : Type u_1} [linear_ordered_field K] (x : {x // 0 < x}) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
Equations