Documentation

Mathlib.Algebra.Ring.InjSurj

Pulling back rings along injective maps, and pushing them forward along surjective maps. #

Distrib class #

@[reducible]
def Function.Injective.distrib {R : Type x} {S : Type u_1} [Mul R] [Add R] [Distrib S] (f : RS) (hf : Function.Injective f) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) :

Pullback a Distrib instance along an injective function. See note [reducible non-instances].

Equations
Instances For
    @[reducible]
    def Function.Surjective.distrib {R : Type x} {S : Type u_1} [Distrib R] [Add S] [Mul S] (f : RS) (hf : Function.Surjective f) (add : ∀ (x y : R), f (x + y) = f x + f y) (mul : ∀ (x y : R), f (x * y) = f x * f y) :

    Pushforward a Distrib instance along a surjective function. See note [reducible non-instances].

    Equations
    Instances For

      Semirings #

      @[reducible]
      def Function.Injective.nonUnitalNonAssocSemiring {β : Type v} [Zero β] [Add β] [Mul β] [SMul β] {α : Type u} [NonUnitalNonAssocSemiring α] (f : βα) (hf : Function.Injective f) (zero : f 0 = 0) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) :

      Pullback a NonUnitalNonAssocRing instance along an injective function. See note [reducible non-instances].

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[reducible]
        def Function.Injective.nonUnitalSemiring {β : Type v} [Zero β] [Add β] [Mul β] [SMul β] {α : Type u} [NonUnitalSemiring α] (f : βα) (hf : Function.Injective f) (zero : f 0 = 0) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) (nsmul : ∀ (x : β) (n : ), f (n x) = n f x) :

        Pullback a NonUnitalSemiring instance along an injective function. See note [reducible non-instances].

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[reducible]
          def Function.Injective.nonAssocSemiring {α : Type u} [NonAssocSemiring α] {β : Type v} [Zero β] [One β] [Mul β] [Add β] [SMul β] [NatCast β] (f : βα) (hf : Function.Injective f) (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 : ∀ (x : β) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) :

          Pullback a NonAssocSemiring instance along an injective function. See note [reducible non-instances].

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[reducible]
            def Function.Injective.semiring {α : Type u} [Semiring α] {β : Type v} [Zero β] [One β] [Add β] [Mul β] [Pow β ] [SMul β] [NatCast β] (f : βα) (hf : Function.Injective f) (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 : ∀ (x : β) (n : ), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) :

            Pullback a Semiring instance along an injective function. See note [reducible non-instances].

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[reducible]
              def Function.Surjective.nonUnitalNonAssocSemiring {β : Type v} [Zero β] [Add β] [Mul β] [SMul β] {α : Type u} [NonUnitalNonAssocSemiring α] (f : αβ) (hf : Function.Surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

              Pushforward a NonUnitalNonAssocSemiring instance along a surjective function. See note [reducible non-instances].

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[reducible]
                def Function.Surjective.nonUnitalSemiring {β : Type v} [Zero β] [Add β] [Mul β] [SMul β] {α : Type u} [NonUnitalSemiring α] (f : αβ) (hf : Function.Surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

                Pushforward a NonUnitalSemiring instance along a surjective function. See note [reducible non-instances].

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[reducible]
                  def Function.Surjective.nonAssocSemiring {α : Type u} [NonAssocSemiring α] {β : Type v} [Zero β] [One β] [Add β] [Mul β] [SMul β] [NatCast β] (f : αβ) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) :

                  Pushforward a NonAssocSemiring instance along a surjective function. See note [reducible non-instances].

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[reducible]
                    def Function.Surjective.semiring {α : Type u} [Semiring α] {β : Type v} [Zero β] [One β] [Add β] [Mul β] [Pow β ] [SMul β] [NatCast β] (f : αβ) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ), f (n x) = n f x) (npow : ∀ (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) :

                    Pushforward a Semiring instance along a surjective function. See note [reducible non-instances].

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[reducible]
                      def Function.Injective.nonUnitalCommSemiring {α : Type u} {γ : Type w} [NonUnitalCommSemiring α] [Zero γ] [Add γ] [Mul γ] [SMul γ] (f : γα) (hf : Function.Injective f) (zero : f 0 = 0) (add : ∀ (x y : γ), f (x + y) = f x + f y) (mul : ∀ (x y : γ), f (x * y) = f x * f y) (nsmul : ∀ (x : γ) (n : ), f (n x) = n f x) :

                      Pullback a NonUnitalCommSemiring instance along an injective function. See note [reducible non-instances].

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[reducible]
                        def Function.Surjective.nonUnitalCommSemiring {α : Type u} {γ : Type w} [NonUnitalCommSemiring α] [Zero γ] [Add γ] [Mul γ] [SMul γ] (f : αγ) (hf : Function.Surjective f) (zero : f 0 = 0) (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) (nsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

                        Pushforward a NonUnitalCommSemiring instance along a surjective function. See note [reducible non-instances].

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[reducible]
                          def Function.Injective.commSemiring {α : Type u} {γ : Type w} [CommSemiring α] [Zero γ] [One γ] [Add γ] [Mul γ] [SMul γ] [NatCast γ] [Pow γ ] (f : γα) (hf : Function.Injective f) (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 : ∀ (x : γ) (n : ), f (n x) = n f x) (npow : ∀ (x : γ) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) :

                          Pullback a CommSemiring instance along an injective function. See note [reducible non-instances].

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[reducible]
                            def Function.Surjective.commSemiring {α : Type u} {γ : Type w} [CommSemiring α] [Zero γ] [One γ] [Add γ] [Mul γ] [SMul γ] [NatCast γ] [Pow γ ] (f : αγ) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ), f (n x) = n f x) (npow : ∀ (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) :

                            Pushforward a CommSemiring instance along a surjective function. See note [reducible non-instances].

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[reducible]
                              def Function.Injective.hasDistribNeg {α : Type u} {β : Type v} [Mul α] [HasDistribNeg α] [Neg β] [Mul β] (f : βα) (hf : Function.Injective f) (neg : ∀ (a : β), f (-a) = -f a) (mul : ∀ (a b : β), f (a * b) = f a * f b) :

                              A type endowed with - and * has distributive negation, if it admits an injective map that preserves - and * to a type which has distributive negation.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[reducible]
                                def Function.Surjective.hasDistribNeg {α : Type u} {β : Type v} [Mul α] [HasDistribNeg α] [Neg β] [Mul β] (f : αβ) (hf : Function.Surjective f) (neg : ∀ (a : α), f (-a) = -f a) (mul : ∀ (a b : α), f (a * b) = f a * f b) :

                                A type endowed with - and * has distributive negation, if it admits a surjective map that preserves - and * from a type which has distributive negation.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.

                                  Rings #

                                  @[reducible]
                                  def Function.Injective.nonUnitalNonAssocRing {α : Type u} {β : Type v} [NonUnitalNonAssocRing α] [Zero β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] (f : βα) (hf : Function.Injective f) (zero : f 0 = 0) (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 : ∀ (x : β) (n : ), f (n x) = n f x) (zsmul : ∀ (x : β) (n : ), f (n x) = n f x) :

                                  Pullback a NonUnitalNonAssocRing instance along an injective function. See note [reducible non-instances].

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[reducible]
                                    def Function.Surjective.nonUnitalNonAssocRing {α : Type u} {β : Type v} [NonUnitalNonAssocRing α] [Zero β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] (f : αβ) (hf : Function.Surjective f) (zero : f 0 = 0) (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 : ∀ (x : α) (n : ), f (n x) = n f x) (zsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

                                    Pushforward a NonUnitalNonAssocRing instance along a surjective function. See note [reducible non-instances].

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[reducible]
                                      def Function.Injective.nonUnitalRing {α : Type u} {β : Type v} [NonUnitalRing α] [Zero β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] (f : βα) (hf : Function.Injective f) (zero : f 0 = 0) (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 : ∀ (x : β) (n : ), f (n x) = n f x) (gsmul : ∀ (x : β) (n : ), f (n x) = n f x) :

                                      Pullback a NonUnitalRing instance along an injective function. See note [reducible non-instances].

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[reducible]
                                        def Function.Surjective.nonUnitalRing {α : Type u} {β : Type v} [NonUnitalRing α] [Zero β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] (f : αβ) (hf : Function.Surjective f) (zero : f 0 = 0) (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 : ∀ (x : α) (n : ), f (n x) = n f x) (gsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

                                        Pushforward a NonUnitalRing instance along a surjective function. See note [reducible non-instances].

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[reducible]
                                          def Function.Injective.nonAssocRing {α : Type u} {β : Type v} [NonAssocRing α] [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [NatCast β] [IntCast β] (f : βα) (hf : Function.Injective f) (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 : ∀ (x : β) (n : ), f (n x) = n f x) (gsmul : ∀ (x : β) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

                                          Pullback a NonAssocRing instance along an injective function. See note [reducible non-instances].

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[reducible]
                                            def Function.Surjective.nonAssocRing {α : Type u} {β : Type v} [NonAssocRing α] [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [NatCast β] [IntCast β] (f : αβ) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ), f (n x) = n f x) (gsmul : ∀ (x : α) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

                                            Pushforward a NonAssocRing instance along a surjective function. See note [reducible non-instances].

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[reducible]
                                              def Function.Injective.ring {α : Type u} {β : Type v} [Ring α] [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] (f : βα) (hf : Function.Injective f) (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 : ∀ (x : β) (n : ), f (n x) = n f x) (zsmul : ∀ (x : β) (n : ), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :
                                              Ring β

                                              Pullback a Ring instance along an injective function. See note [reducible non-instances].

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[reducible]
                                                def Function.Surjective.ring {α : Type u} {β : Type v} [Ring α] [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] (f : αβ) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ), f (n x) = n f x) (zsmul : ∀ (x : α) (n : ), f (n x) = n f x) (npow : ∀ (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :
                                                Ring β

                                                Pushforward a Ring instance along a surjective function. See note [reducible non-instances].

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[reducible]
                                                  def Function.Injective.nonUnitalCommRing {α : Type u} {β : Type v} [NonUnitalCommRing α] [Zero β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] (f : βα) (hf : Function.Injective f) (zero : f 0 = 0) (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 : ∀ (x : β) (n : ), f (n x) = n f x) (zsmul : ∀ (x : β) (n : ), f (n x) = n f x) :

                                                  Pullback a NonUnitalCommRing instance along an injective function. See note [reducible non-instances].

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[reducible]
                                                    def Function.Surjective.nonUnitalCommRing {α : Type u} {β : Type v} [NonUnitalCommRing α] [Zero β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] (f : αβ) (hf : Function.Surjective f) (zero : f 0 = 0) (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 : ∀ (x : α) (n : ), f (n x) = n f x) (zsmul : ∀ (x : α) (n : ), f (n x) = n f x) :

                                                    Pushforward a NonUnitalCommRing instance along a surjective function. See note [reducible non-instances].

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[reducible]
                                                      def Function.Injective.commRing {α : Type u} {β : Type v} [CommRing α] [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] (f : βα) (hf : Function.Injective f) (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 : ∀ (x : β) (n : ), f (n x) = n f x) (zsmul : ∀ (x : β) (n : ), f (n x) = n f x) (npow : ∀ (x : β) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

                                                      Pullback a CommRing instance along an injective function. See note [reducible non-instances].

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[reducible]
                                                        def Function.Surjective.commRing {α : Type u} {β : Type v} [CommRing α] [Zero β] [One β] [Add β] [Mul β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] (f : αβ) (hf : Function.Surjective f) (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 : ∀ (x : α) (n : ), f (n x) = n f x) (zsmul : ∀ (x : α) (n : ), f (n x) = n f x) (npow : ∀ (x : α) (n : ), f (x ^ n) = f x ^ n) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

                                                        Pushforward a CommRing instance along a surjective function. See note [reducible non-instances].

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For