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.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
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
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
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
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
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
Equations
instance Positive.instDistribSubtypeLtOfNat {R : Type u_2} [StrictOrderedSemiring R] :
Distrib { x : R // 0 < x }
Equations
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
Equations

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

Equations