mathlib3 documentation

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]
Equations
@[simp, norm_cast]
theorem positive.coe_add {M : Type u_1} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] (x y : {x // 0 < x}) :
(x + y) = x + y
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem positive.coe_mul {R : Type u_2} [strict_ordered_semiring R] (x y : {x // 0 < x}) :
(x * y) = x * y
@[protected, instance]
def positive.nat.has_pow {R : Type u_2} [strict_ordered_semiring R] :
has_pow {x // 0 < x}
Equations
@[simp]
theorem positive.coe_pow {R : Type u_2} [strict_ordered_semiring R] (x : {x // 0 < x}) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem positive.coe_one {R : Type u_2} [strict_ordered_semiring R] [nontrivial R] :
1 = 1
@[protected, instance]
Equations
@[protected, instance]
Equations