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.instAddSubtypeLtToLTOfNatToOfNat0ToZero {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

Add { x // 0 < x }

source

@[simp]

theorem Positive.coe_add {M : Type u_1} [AddMonoid M] [Preorder M] [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

source

instance Positive.addSemigroup {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

AddSemigroup { x // 0 < x }

source

instance Positive.addCommSemigroup {M : Type u_4} [AddCommMonoid M] [Preorder M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

AddCommSemigroup { x // 0 < x }

source

instance Positive.addLeftCancelSemigroup {M : Type u_4} [AddLeftCancelMonoid M] [Preorder M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

AddLeftCancelSemigroup { x // 0 < x }

source

instance Positive.addRightCancelSemigroup {M : Type u_4} [AddRightCancelMonoid M] [Preorder M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :

AddRightCancelSemigroup { x // 0 < x }

source

instance Positive.covariantClass_add_lt {M : Type u_1} [AddMonoid M] [Preorder M] [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

source

instance Positive.covariantClass_swap_add_lt {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [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

source

instance Positive.contravariantClass_add_lt {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [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

source

instance Positive.contravariantClass_swap_add_lt {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [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

source

instance Positive.contravariantClass_add_le {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [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

source

instance Positive.contravariantClass_swap_add_le {M : Type u_1} [AddMonoid M] [Preorder M] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [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

source

instance Positive.covariantClass_add_le {M : Type u_1} [AddMonoid M] [PartialOrder M] [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

source

instance Positive.instMulSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring {R : Type u_2} [StrictOrderedSemiring R] :

Mul { x // 0 < x }

source

@[simp]

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

↑(x * y) = ↑x * ↑y

source

instance Positive.instPowSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiringNat {R : Type u_2} [StrictOrderedSemiring R] :

Pow { x // 0 < x } ℕ

source

@[simp]

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

↑(x ^ n) = ↑x ^ n

source

instance Positive.instSemigroupSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring {R : Type u_2} [StrictOrderedSemiring R] :

Semigroup { x // 0 < x }

source

instance Positive.instDistribSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring {R : Type u_2} [StrictOrderedSemiring R] :

Distrib { x // 0 < x }

source

instance Positive.instOneSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring {R : Type u_2} [StrictOrderedSemiring R] [Nontrivial R] :

One { x // 0 < x }

source

@[simp]

theorem Positive.val_one {R : Type u_2} [StrictOrderedSemiring R] [Nontrivial R] :

↑1 = 1

source

instance Positive.instMonoidSubtypeLtToLTToPreorderToPartialOrderOfNatToOfNat0ToZeroToMonoidWithZeroToSemiring {R : Type u_2} [StrictOrderedSemiring R] [Nontrivial R] :

Monoid { x // 0 < x }

source

instance Positive.orderedCommMonoid {R : Type u_2} [StrictOrderedCommSemiring R] [Nontrivial R] :

OrderedCommMonoid { x // 0 < x }

source

instance Positive.linearOrderedCancelCommMonoid {R : Type u_2} [LinearOrderedCommSemiring R] :

LinearOrderedCancelCommMonoid { x // 0 < x }

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