mathlib3documentation

algebra.order.positive.ring

Algebraic structures on the set of positive numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define various instances (add_semigroup, ordered_comm_monoid etc) on the type {x : R // 0 < x}. In each case we try to require the weakest possible typeclass assumptions on R but possibly, there is a room for improvements.

@[protected, instance]
has_add {x // 0 < x}
Equations
@[simp, norm_cast]
theorem positive.coe_add {M : Type u_1} [add_monoid M] [preorder M] (x y : {x // 0 < x}) :
(x + y) = x + y
@[protected, instance]
add_semigroup {x // 0 < x}
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
covariant_class {x // 0 < x} {x // 0 < x} has_lt.lt
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def positive.subtype.has_mul {R : Type u_2}  :
has_mul {x // 0 < x}
Equations
@[simp]
theorem positive.coe_mul {R : Type u_2} (x y : {x // 0 < x}) :
(x * y) = x * y
@[protected, instance]
def positive.nat.has_pow {R : Type u_2}  :
has_pow {x // 0 < x}
Equations
@[simp]
theorem positive.coe_pow {R : Type u_2} (x : {x // 0 < x}) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
def positive.subtype.semigroup {R : Type u_2}  :
semigroup {x // 0 < x}
Equations
@[protected, instance]
def positive.subtype.distrib {R : Type u_2}  :
distrib {x // 0 < x}
Equations
@[protected, instance]
def positive.subtype.has_one {R : Type u_2} [nontrivial R] :
has_one {x // 0 < x}
Equations
@[simp]
theorem positive.coe_one {R : Type u_2} [nontrivial R] :
1 = 1
@[protected, instance]
def positive.subtype.monoid {R : Type u_2} [nontrivial R] :
monoid {x // 0 < x}
Equations
@[protected, instance]
Equations
@[protected, instance]

If R is a nontrivial linear ordered commutative semiring, then {x : R // 0 < x} is a linear ordered cancellative commutative monoid.

Equations