Documentation

Mathlib.Algebra.Order.Ring.InjSurj

Pulling back ordered rings along injective maps #

@[reducible, inline]
abbrev Function.Injective.orderedSemiring {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [SMul β] [Pow β ] [NatCast β] (f : βα) (hf : Function.Injective f) [OrderedSemiring α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = n) :

Pullback an OrderedSemiring under an injective map.

Equations
Instances For
    @[reducible, inline]
    abbrev Function.Injective.orderedCommSemiring {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [SMul β] [Pow β ] [NatCast β] (f : βα) (hf : Function.Injective f) [OrderedCommSemiring α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = n) :

    Pullback an OrderedCommSemiring under an injective map.

    Equations
    Instances For
      @[reducible, inline]
      abbrev Function.Injective.orderedRing {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] (f : βα) (hf : Function.Injective f) [OrderedRing α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (zsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = n) (intCast : ∀ (n : ), f n = n) :

      Pullback an OrderedRing under an injective map.

      Equations
      Instances For
        @[reducible, inline]
        abbrev Function.Injective.orderedCommRing {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] (f : βα) (hf : Function.Injective f) [OrderedCommRing α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (zsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = n) (intCast : ∀ (n : ), f n = n) :

        Pullback an OrderedCommRing under an injective map.

        Equations
        Instances For
          @[reducible, inline]
          abbrev Function.Injective.strictOrderedSemiring {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [SMul β] [Pow β ] [NatCast β] (f : βα) (hf : Function.Injective f) [StrictOrderedSemiring α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = n) :

          Pullback a StrictOrderedSemiring under an injective map.

          Equations
          Instances For
            @[reducible, inline]
            abbrev Function.Injective.strictOrderedCommSemiring {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [SMul β] [Pow β ] [NatCast β] (f : βα) (hf : Function.Injective f) [StrictOrderedCommSemiring α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = n) :

            Pullback a strictOrderedCommSemiring under an injective map.

            Equations
            Instances For
              @[reducible, inline]
              abbrev Function.Injective.strictOrderedRing {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] (f : βα) (hf : Function.Injective f) [StrictOrderedRing α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (zsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = n) (intCast : ∀ (n : ), f n = n) :

              Pullback a StrictOrderedRing under an injective map.

              Equations
              Instances For
                @[reducible, inline]
                abbrev Function.Injective.strictOrderedCommRing {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] (f : βα) (hf : Function.Injective f) [StrictOrderedCommRing α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (zsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = n) (intCast : ∀ (n : ), f n = n) :

                Pullback a StrictOrderedCommRing under an injective map.

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev Function.Injective.linearOrderedSemiring {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [SMul β] [Pow β ] [NatCast β] [Sup β] [Inf β] (f : βα) (hf : Function.Injective f) [LinearOrderedSemiring α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = 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 LinearOrderedSemiring under an injective map.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[reducible, inline]
                    abbrev Function.Injective.linearOrderedCommSemiring {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [SMul β] [Pow β ] [NatCast β] [Sup β] [Inf β] (f : βα) (hf : Function.Injective f) [LinearOrderedCommSemiring α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = 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 LinearOrderedSemiring under an injective map.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[reducible, inline]
                      abbrev Function.Injective.linearOrderedRing {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] [Sup β] [Inf β] (f : βα) (hf : Function.Injective f) [LinearOrderedRing α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (zsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = n) (intCast : ∀ (n : ), f n = 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 LinearOrderedRing under an injective map.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[reducible, inline]
                        abbrev Function.Injective.linearOrderedCommRing {α : Type u_1} {β : Type u_2} [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] [Sup β] [Inf β] (f : βα) (hf : Function.Injective f) [LinearOrderedCommRing α] (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (nsmul : ∀ (n : ) (x : β), f (n x) = n f x) (zsmul : ∀ (n : ) (x : β), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (natCast : ∀ (n : ), f n = n) (intCast : ∀ (n : ), f n = 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 LinearOrderedCommRing under an injective map.

                        Equations
                        Instances For