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.

@[implicit_reducible]

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

@[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

@[implicit_reducible]

instance Positive.addSemigroup {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] : AddSemigroup { x : M // 0 < x }

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

instance Positive.addLeftStrictMono {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] : AddLeftStrictMono { x : M // 0 < x }

instance Positive.addRightStrictMono {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] : AddRightStrictMono { x : M // 0 < x }

instance Positive.addLeftReflectLT {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftReflectLT M] : AddLeftReflectLT { x : M // 0 < x }

instance Positive.addRightReflectLT {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightReflectLT M] : AddRightReflectLT { x : M // 0 < x }

instance Positive.addLeftReflectLE {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftReflectLE M] : AddLeftReflectLE { x : M // 0 < x }

instance Positive.addRightReflectLE {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddRightReflectLE M] : AddRightReflectLE { x : M // 0 < x }

instance Positive.addLeftMono {M : Type u_1} [AddMonoid M] [PartialOrder M] [AddLeftStrictMono M] : AddLeftMono { x : M // 0 < x }

@[implicit_reducible]

instance Positive.instMulSubtypeLtOfNat_mathlib {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : Mul { x : R // 0 < x }

@[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

@[implicit_reducible]

instance Positive.instPowSubtypeLtOfNatNat_mathlib {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : Pow { x : R // 0 < x } ℕ

@[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

@[implicit_reducible]

instance Positive.instSemigroupSubtypeLtOfNat {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : Semigroup { x : R // 0 < x }

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

theorem Positive.val_one {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : ↑1 = 1

@[implicit_reducible]

instance Positive.instMonoidSubtypeLtOfNat {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : Monoid { x : R // 0 < x }

@[implicit_reducible]

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

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

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.