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.

source
instance Positive.instAddSubtypeLtOfNat_mathlib {M : Type u_1} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] :
Add { x : M // 0 < x }
Equations
    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
      source
      instance Positive.addCommSemigroup {M : Type u_3} [AddCommMonoid M] [Preorder M] [AddLeftStrictMono M] :
      AddCommSemigroup { x : M // 0 < x }
      Equations
        source
        instance Positive.addLeftCancelSemigroup {M : Type u_3} [AddLeftCancelMonoid M] [Preorder M] [AddLeftStrictMono M] :
        AddLeftCancelSemigroup { x : M // 0 < x }
        Equations
          source
          instance Positive.addRightCancelSemigroup {M : Type u_3} [AddRightCancelMonoid M] [Preorder M] [AddLeftStrictMono M] :
          AddRightCancelSemigroup { x : M // 0 < x }
          Equations
            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
              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
                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
                  source
                  instance Positive.instDistribSubtypeLtOfNat {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
                  Distrib { x : R // 0 < x }
                  Equations
                    source
                    instance Positive.instOneSubtypeLtOfNat_mathlib {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] :
                    One { x : R // 0 < x }
                    Equations
                      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
                        source
                        instance Positive.commMonoid {R : Type u_2} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
                        CommMonoid { x : R // 0 < x }
                        Equations
                          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.