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.instAddSubtypeLtOfNat_mathlib {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] : Add { x : M // 0 < x }

Equations

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

@[simp]

theorem Positive.coe_add {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] (x : { x : M // 0 < x }) (y : { x : M // 0 < x }) : ↑(x + y) = ↑x + ↑y

instance Positive.addSemigroup {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] : AddSemigroup { x : M // 0 < x }

Equations

• Positive.addSemigroup = Function.Injective.addSemigroup (fun (a : { x : M // 0 < x }) => ↑a) ⋯ ⋯

instance Positive.addCommSemigroup {M : Type u_3} [AddCommMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] : AddCommSemigroup { x : M // 0 < x }

Equations

• Positive.addCommSemigroup = Function.Injective.addCommSemigroup (fun (a : { x : M // 0 < x }) => ↑a) ⋯ ⋯

instance Positive.addLeftCancelSemigroup {M : Type u_3} [AddLeftCancelMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] : AddLeftCancelSemigroup { x : M // 0 < x }

Equations

• Positive.addLeftCancelSemigroup = Function.Injective.addLeftCancelSemigroup (fun (a : { x : M // 0 < x }) => ↑a) ⋯ ⋯

instance Positive.addRightCancelSemigroup {M : Type u_3} [AddRightCancelMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] : AddRightCancelSemigroup { x : M // 0 < x }

Equations

• Positive.addRightCancelSemigroup = Function.Injective.addRightCancelSemigroup (fun (a : { x : M // 0 < x }) => ↑a) ⋯ ⋯

instance Positive.covariantClass_add_lt {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] : CovariantClass { x : M // 0 < x } { x : M // 0 < x } (fun (x1 x2 : { x : M // 0 < x }) => x1 + x2) fun (x1 x2 : { x : M // 0 < x }) => x1 < x2

Equations

• ⋯ = ⋯

instance Positive.covariantClass_swap_add_lt {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] : CovariantClass { x : M // 0 < x } { x : M // 0 < x } (Function.swap fun (x1 x2 : { x : M // 0 < x }) => x1 + x2) fun (x1 x2 : { x : M // 0 < x }) => x1 < x2

Equations

• ⋯ = ⋯

instance Positive.contravariantClass_add_lt {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [ContravariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] : ContravariantClass { x : M // 0 < x } { x : M // 0 < x } (fun (x1 x2 : { x : M // 0 < x }) => x1 + x2) fun (x1 x2 : { x : M // 0 < x }) => x1 < x2

Equations

• ⋯ = ⋯

instance Positive.contravariantClass_swap_add_lt {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [ContravariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] : ContravariantClass { x : M // 0 < x } { x : M // 0 < x } (Function.swap fun (x1 x2 : { x : M // 0 < x }) => x1 + x2) fun (x1 x2 : { x : M // 0 < x }) => x1 < x2

Equations

• ⋯ = ⋯

instance Positive.contravariantClass_add_le {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [ContravariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] : ContravariantClass { x : M // 0 < x } { x : M // 0 < x } (fun (x1 x2 : { x : M // 0 < x }) => x1 + x2) fun (x1 x2 : { x : M // 0 < x }) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance Positive.contravariantClass_swap_add_le {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [ContravariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2] : ContravariantClass { x : M // 0 < x } { x : M // 0 < x } (Function.swap fun (x1 x2 : { x : M // 0 < x }) => x1 + x2) fun (x1 x2 : { x : M // 0 < x }) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance Positive.covariantClass_add_le {M : Type u_1} [AddMonoid M] [PartialOrder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] : CovariantClass { x : M // 0 < x } { x : M // 0 < x } (fun (x1 x2 : { x : M // 0 < x }) => x1 + x2) fun (x1 x2 : { x : M // 0 < x }) => x1 ≤ x2

Equations

• ⋯ = ⋯

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

Equations

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

@[simp]

theorem Positive.val_mul {R : Type u_2} [StrictOrderedSemiring R] (x : { x : R // 0 < x }) (y : { x : R // 0 < x }) : ↑(x * y) = ↑x * ↑y

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

Equations

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

@[simp]

theorem Positive.val_pow {R : Type u_2} [StrictOrderedSemiring R] (x : { x : R // 0 < x }) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

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

Equations

• Positive.instSemigroupSubtypeLtOfNat = Function.Injective.semigroup Subtype.val ⋯ ⋯

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

Equations

• Positive.instDistribSubtypeLtOfNat = Function.Injective.distrib (fun (a : { x : R // 0 < x }) => ↑a) ⋯ ⋯ ⋯

instance Positive.instOneSubtypeLtOfNat {R : Type u_2} [StrictOrderedSemiring R] : One { x : R // 0 < x }

Equations

• Positive.instOneSubtypeLtOfNat = { one := ⟨1, ⋯⟩ }

@[simp]

theorem Positive.val_one {R : Type u_2} [StrictOrderedSemiring R] : ↑1 = 1

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

Equations

• Positive.instMonoidSubtypeLtOfNat = Function.Injective.monoid (fun (a : { x : R // 0 < x }) => ↑a) ⋯ ⋯ ⋯ ⋯

instance Positive.orderedCommMonoid {R : Type u_2} [StrictOrderedCommSemiring R] : OrderedCommMonoid { x : R // 0 < x }

Equations

• Positive.orderedCommMonoid = OrderedCommMonoid.mk ⋯

instance Positive.linearOrderedCancelCommMonoid {R : Type u_2} [LinearOrderedCommSemiring R] : LinearOrderedCancelCommMonoid { 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.

Equations

• Positive.linearOrderedCancelCommMonoid = LinearOrderedCancelCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯