Documentation

Mathlib.Algebra.Order.Monoid.Basic

Ordered monoids #

This file develops some additional material on ordered monoids.

@[reducible, inline]
abbrev Function.Injective.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] {β : Type u_2} [Zero β] [Add β] [SMul β] (f : βα) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) :

Pullback an OrderedAddCommMonoid under an injective map.

Equations
Instances For
    @[reducible, inline]
    abbrev Function.Injective.orderedCommMonoid {α : Type u} [OrderedCommMonoid α] {β : Type u_2} [One β] [Mul β] [Pow β ] (f : βα) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) :

    Pullback an OrderedCommMonoid under an injective map. See note [reducible non-instances].

    Equations
    Instances For
      @[reducible, inline]
      abbrev Function.Injective.orderedCancelAddCommMonoid {α : Type u} {β : Type u_1} [OrderedCancelAddCommMonoid α] [Zero β] [Add β] [SMul β] (f : βα) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) :

      Pullback an OrderedCancelAddCommMonoid under an injective map.

      Equations
      Instances For
        @[reducible, inline]
        abbrev Function.Injective.orderedCancelCommMonoid {α : Type u} {β : Type u_1} [OrderedCancelCommMonoid α] [One β] [Mul β] [Pow β ] (f : βα) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) :

        Pullback an OrderedCancelCommMonoid under an injective map. See note [reducible non-instances].

        Equations
        Instances For
          @[reducible, inline]
          abbrev Function.Injective.linearOrderedAddCommMonoid {α : Type u} [LinearOrderedAddCommMonoid α] {β : Type u_2} [Zero β] [Add β] [SMul β] [Sup β] [Inf β] (f : βα) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) (sup : ∀ (x y : β), f (x y) = max (f x) (f y)) (inf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

          Pullback an OrderedAddCommMonoid under an injective map.

          Equations
          Instances For
            @[reducible, inline]
            abbrev Function.Injective.linearOrderedCommMonoid {α : Type u} [LinearOrderedCommMonoid α] {β : Type u_2} [One β] [Mul β] [Pow β ] [Sup β] [Inf β] (f : βα) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (sup : ∀ (x y : β), f (x y) = max (f x) (f y)) (inf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

            Pullback a LinearOrderedCommMonoid under an injective map. See note [reducible non-instances].

            Equations
            Instances For
              @[reducible, inline]
              abbrev Function.Injective.linearOrderedCancelAddCommMonoid {α : Type u} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [Zero β] [Add β] [SMul β] [Sup β] [Inf β] (f : βα) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (npow : ∀ (x : β) (n : ), f (n x) = n f x) (hsup : ∀ (x y : β), f (x y) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

              Pullback a LinearOrderedCancelAddCommMonoid under an injective map.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[reducible, inline]
                abbrev Function.Injective.linearOrderedCancelCommMonoid {α : Type u} {β : Type u_1} [LinearOrderedCancelCommMonoid α] [One β] [Mul β] [Pow β ] [Sup β] [Inf β] (f : βα) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = f x * f y) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (hsup : ∀ (x y : β), f (x y) = max (f x) (f y)) (hinf : ∀ (x y : β), f (x y) = min (f x) (f y)) :

                Pullback a LinearOrderedCancelCommMonoid under an injective map. See note [reducible non-instances].

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def OrderEmbedding.addLeft {α : Type u_2} [Add α] [LinearOrder α] [AddLeftStrictMono α] (m : α) :
                  α ↪o α

                  The order embedding sending b to a + b, for some fixed a. See also OrderIso.addLeft when working in an additive ordered group.

                  Equations
                  Instances For
                    @[simp]
                    theorem OrderEmbedding.addLeft_apply {α : Type u_2} [Add α] [LinearOrder α] [AddLeftStrictMono α] (m : α) (n : α) :
                    @[simp]
                    theorem OrderEmbedding.mulLeft_apply {α : Type u_2} [Mul α] [LinearOrder α] [MulLeftStrictMono α] (m : α) (n : α) :
                    def OrderEmbedding.mulLeft {α : Type u_2} [Mul α] [LinearOrder α] [MulLeftStrictMono α] (m : α) :
                    α ↪o α

                    The order embedding sending b to a * b, for some fixed a. See also OrderIso.mulLeft when working in an ordered group.

                    Equations
                    Instances For
                      def OrderEmbedding.addRight {α : Type u_2} [Add α] [LinearOrder α] [AddRightStrictMono α] (m : α) :
                      α ↪o α

                      The order embedding sending b to b + a, for some fixed a. See also OrderIso.addRight when working in an additive ordered group.

                      Equations
                      Instances For
                        @[simp]
                        theorem OrderEmbedding.addRight_apply {α : Type u_2} [Add α] [LinearOrder α] [AddRightStrictMono α] (m : α) (n : α) :
                        @[simp]
                        theorem OrderEmbedding.mulRight_apply {α : Type u_2} [Mul α] [LinearOrder α] [MulRightStrictMono α] (m : α) (n : α) :
                        def OrderEmbedding.mulRight {α : Type u_2} [Mul α] [LinearOrder α] [MulRightStrictMono α] (m : α) :
                        α ↪o α

                        The order embedding sending b to b * a, for some fixed a. See also OrderIso.mulRight when working in an ordered group.

                        Equations
                        Instances For