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.

source
@[protected, instance]
def positive.subtype.has_add {M : Type u_1} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] :
has_add {x // 0 < x}
Equations
source
@[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
source
@[protected, instance]
def positive.subtype.add_semigroup {M : Type u_1} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] :
add_semigroup {x // 0 < x}
Equations
source
@[protected, instance]
def positive.subtype.add_comm_semigroup {M : Type u_1} [add_comm_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] :
add_comm_semigroup {x // 0 < x}
Equations
source
@[protected, instance]
def positive.subtype.add_left_cancel_semigroup {M : Type u_1} [add_left_cancel_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] :
add_left_cancel_semigroup {x // 0 < x}
Equations
source
@[protected, instance]
def positive.subtype.add_right_cancel_semigroup {M : Type u_1} [add_right_cancel_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] :
add_right_cancel_semigroup {x // 0 < x}
Equations
source
@[protected, instance]
def positive.covariant_class_add_lt {M : Type u_1} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] :
covariant_class {x // 0 < x} {x // 0 < x} has_add.add has_lt.lt
source
@[protected, instance]
def positive.covariant_class_swap_add_lt {M : Type u_1} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] [covariant_class M M (function.swap has_add.add) has_lt.lt] :
covariant_class {x // 0 < x} {x // 0 < x} (function.swap has_add.add) has_lt.lt
source
@[protected, instance]
def positive.contravariant_class_add_lt {M : Type u_1} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] [contravariant_class M M has_add.add has_lt.lt] :
contravariant_class {x // 0 < x} {x // 0 < x} has_add.add has_lt.lt
source
@[protected, instance]
def positive.contravariant_class_swap_add_lt {M : Type u_1} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] [contravariant_class M M (function.swap has_add.add) has_lt.lt] :
contravariant_class {x // 0 < x} {x // 0 < x} (function.swap has_add.add) has_lt.lt
source
@[protected, instance]
def positive.contravariant_class_add_le {M : Type u_1} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] [contravariant_class M M has_add.add has_le.le] :
contravariant_class {x // 0 < x} {x // 0 < x} has_add.add has_le.le
source
@[protected, instance]
def positive.contravariant_class_swap_add_le {M : Type u_1} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] [contravariant_class M M (function.swap has_add.add) has_le.le] :
contravariant_class {x // 0 < x} {x // 0 < x} (function.swap has_add.add) has_le.le
source
@[protected, instance]
def positive.covariant_class_add_le {M : Type u_1} [add_monoid M] [partial_order M] [covariant_class M M has_add.add has_lt.lt] :
covariant_class {x // 0 < x} {x // 0 < x} has_add.add has_le.le
source
@[protected, instance]
def positive.subtype.has_mul {R : Type u_2} [strict_ordered_semiring R] :
has_mul {x // 0 < x}
Equations
source
@[simp]
theorem positive.coe_mul {R : Type u_2} [strict_ordered_semiring R] (x y : {x // 0 < x}) :
↑(x * y) = ↑x * ↑y
source
@[protected, instance]
def positive.nat.has_pow {R : Type u_2} [strict_ordered_semiring R] :
has_pow {x // 0 < x} ℕ
Equations
source
@[simp]
theorem positive.coe_pow {R : Type u_2} [strict_ordered_semiring R] (x : {x // 0 < x}) (n : ℕ) :
↑(x ^ n) = ↑x ^ n
source
@[protected, instance]
def positive.subtype.semigroup {R : Type u_2} [strict_ordered_semiring R] :
semigroup {x // 0 < x}
Equations
source
@[protected, instance]
def positive.subtype.distrib {R : Type u_2} [strict_ordered_semiring R] :
distrib {x // 0 < x}
Equations
source
@[protected, instance]
def positive.subtype.has_one {R : Type u_2} [strict_ordered_semiring R] [nontrivial R] :
has_one {x // 0 < x}
Equations
source
@[simp]
theorem positive.coe_one {R : Type u_2} [strict_ordered_semiring R] [nontrivial R] :
↑1 = 1
source
@[protected, instance]
def positive.subtype.monoid {R : Type u_2} [strict_ordered_semiring R] [nontrivial R] :
monoid {x // 0 < x}
Equations
source
@[protected, instance]
def positive.subtype.ordered_comm_monoid {R : Type u_2} [strict_ordered_comm_semiring R] [nontrivial R] :
ordered_comm_monoid {x // 0 < x}
Equations
source
@[protected, instance]
def positive.subtype.linear_ordered_cancel_comm_monoid {R : Type u_2} [linear_ordered_comm_semiring R] :
linear_ordered_cancel_comm_monoid {x // 0 < x}

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

Equations