# 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.

source
instance Positive.instAddSubtypeLtOfNat_mathlib {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] :
Add { x : M // 0 < x }
Equations

- Positive.instAddSubtypeLtOfNat_mathlib = { add := fun (x y : { x : M // 0 < x }) => ⟨↑x + ↑y, ⋯⟩ }

source
@[simp]
theorem Positive.coe_add {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] (x y : { x : M // 0 < x }) :
↑(x + y) = ↑x + ↑y
source
instance Positive.addSemigroup {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] :
AddSemigroup { x : M // 0 < x }
Equations

- Positive.addSemigroup = { toAdd := Positive.instAddSubtypeLtOfNat_mathlib, add_assoc := ⋯ }

source
instance Positive.addCommSemigroup {M : Type u_3} [AddCommMonoid M] [Preorder M] [AddLeftStrictMono M] :
AddCommSemigroup { x : M // 0 < x }
Equations

- Positive.addCommSemigroup = { toAddSemigroup := Positive.addSemigroup, add_comm := ⋯ }

source
instance Positive.addLeftCancelSemigroup {M : Type u_3} [AddLeftCancelMonoid M] [Preorder M] [AddLeftStrictMono M] :
AddLeftCancelSemigroup { x : M // 0 < x }
Equations

- Positive.addLeftCancelSemigroup = { toAddSemigroup := Positive.addSemigroup, toIsLeftCancelAdd := ⋯ }

source
instance Positive.addRightCancelSemigroup {M : Type u_3} [AddRightCancelMonoid M] [Preorder M] [AddLeftStrictMono M] :
AddRightCancelSemigroup { x : M // 0 < x }
Equations

- Positive.addRightCancelSemigroup = { toAddSemigroup := Positive.addSemigroup, toIsRightCancelAdd := ⋯ }

source
instance Positive.addLeftStrictMono {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] :
AddLeftStrictMono { x : M // 0 < x }
source
instance Positive.addRightStrictMono {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] :
AddRightStrictMono { x : M // 0 < x }
source
instance Positive.addLeftReflectLT {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftReflectLT M] :
AddLeftReflectLT { x : M // 0 < x }
source
instance Positive.addRightReflectLT {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightReflectLT M] :
AddRightReflectLT { x : M // 0 < x }
source
instance Positive.addLeftReflectLE {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftReflectLE M] :
AddLeftReflectLE { x : M // 0 < x }
source
instance Positive.addRightReflectLE {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightReflectLE M] :
AddRightReflectLE { x : M // 0 < x }
source
instance Positive.addLeftMono {M : Type u_1} [AddMonoid M] [PartialOrder M] [AddLeftStrictMono M] :
AddLeftMono { x : M // 0 < x }
source
instance Positive.instMulSubtypeLtOfNat_mathlib {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
Mul { x : R // 0 < x }
Equations

- Positive.instMulSubtypeLtOfNat_mathlib = { mul := fun (x y : { x : R // 0 < x }) => ⟨↑x * ↑y, ⋯⟩ }

source
@[simp]
theorem Positive.val_mul {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (x y : { x : R // 0 < x }) :
↑(x * y) = ↑x * ↑y
source
instance Positive.instPowSubtypeLtOfNatNat_mathlib {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
Pow { x : R // 0 < x } ℕ
Equations

- Positive.instPowSubtypeLtOfNatNat_mathlib = { pow := fun (x : { x : R // 0 < x }) (n : ℕ) => ⟨↑x ^ n, ⋯⟩ }

source
@[simp]
theorem Positive.val_pow {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (x : { x : R // 0 < x }) (n : ℕ) :
↑(x ^ n) = ↑x ^ n
source
instance Positive.instSemigroupSubtypeLtOfNat {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
Semigroup { x : R // 0 < x }
Equations

- Positive.instSemigroupSubtypeLtOfNat = { toMul := Positive.instMulSubtypeLtOfNat_mathlib, mul_assoc := ⋯ }

source
instance Positive.instDistribSubtypeLtOfNat {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
Distrib { x : R // 0 < x }
Equations

- Positive.instDistribSubtypeLtOfNat = { toMul := Positive.instMulSubtypeLtOfNat_mathlib, toAdd := Positive.instAddSubtypeLtOfNat_mathlib, left_distrib := ⋯, right_distrib := ⋯ }

source
instance Positive.instOneSubtypeLtOfNat_mathlib {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
One { x : R // 0 < x }
Equations

- Positive.instOneSubtypeLtOfNat_mathlib = { one := ⟨1, ⋯⟩ }

source
@[simp]
theorem Positive.val_one {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
↑1 = 1
source
instance Positive.instMonoidSubtypeLtOfNat {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
Monoid { x : R // 0 < x }
Equations

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

source
instance Positive.commMonoid {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
CommMonoid { x : R // 0 < x }
Equations

- Positive.commMonoid = { toMonoid := Positive.instMonoidSubtypeLtOfNat, mul_comm := ⋯ }

source
instance Positive.isOrderedMonoid {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
IsOrderedMonoid { x : R // 0 < x }
source
instance Positive.isOrderedCancelMonoid {R : Type u_2} [CommSemiring R] [LinearOrder R] [IsStrictOrderedRing R] :
IsOrderedCancelMonoid { x : R // 0 < x }

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