# Documentation

Mathlib.Algebra.Order.Positive.Ring

# Algebraic structures on the set of positive numbers #

In this file we define various instances (AddSemigroup, OrderedCommMonoid 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.

instance Positive.instAddSubtypeLtToLTOfNatToOfNat0ToZero {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
Add { x // 0 < x }
Equations
• Positive.instAddSubtypeLtToLTOfNatToOfNat0ToZero = { add := fun x y => { val := x + y, property := (_ : 0 < x + y) } }
@[simp]
theorem Positive.coe_add {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (x : { x // 0 < x }) (y : { x // 0 < x }) :
↑(x + y) = x + y
instance Positive.addSemigroup {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
AddSemigroup { x // 0 < x }
Equations
instance Positive.addCommSemigroup {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
AddCommSemigroup { x // 0 < x }
Equations
instance Positive.addLeftCancelSemigroup {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
Equations
instance Positive.addRightCancelSemigroup {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
Equations
instance Positive.covariantClass_add_lt {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass { x // 0 < x } { x // 0 < x } (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance Positive.covariantClass_swap_add_lt {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass { x // 0 < x } { x // 0 < x } (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance Positive.contravariantClass_add_lt {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
ContravariantClass { x // 0 < x } { x // 0 < x } (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance Positive.contravariantClass_swap_add_lt {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
ContravariantClass { x // 0 < x } { x // 0 < x } (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance Positive.contravariantClass_add_le {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] :
ContravariantClass { x // 0 < x } { x // 0 < x } (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance Positive.contravariantClass_swap_add_le {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : ContravariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
ContravariantClass { x // 0 < x } { x // 0 < x } (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance Positive.covariantClass_add_le {M : Type u_1} [inst : ] [inst : ] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass { x // 0 < x } { x // 0 < x } (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
Equations
• Positive.instMulSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring = { mul := fun x y => { val := x * y, property := (_ : 0 < x * y) } }
@[simp]
theorem Positive.val_mul {R : Type u_1} [inst : ] (x : { x // 0 < x }) (y : { x // 0 < x }) :
↑(x * y) = x * y
Equations
• Positive.instPowSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiringNat = { pow := fun x n => { val := x ^ n, property := (_ : 0 < x ^ n) } }
@[simp]
theorem Positive.val_pow {R : Type u_1} [inst : ] (x : { x // 0 < x }) (n : ) :
↑(x ^ n) = x ^ n
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• Positive.instOneSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring = { one := { val := 1, property := (_ : 0 < 1) } }
@[simp]
theorem Positive.val_one {R : Type u_1} [inst : ] [inst : ] :
1 = 1
Equations
• One or more equations did not get rendered due to their size.
instance Positive.orderedCommMonoid {R : Type u_1} [inst : ] [inst : ] :
OrderedCommMonoid { x // 0 < x }
Equations
• One or more equations did not get rendered due to their size.

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

Equations
• One or more equations did not get rendered due to their size.