Documentation

Mathlib.Algebra.Ring.InjSurj

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

theorem Function.Injective.leftDistribClass {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Mul α] [Add α] [LeftDistribClass α] (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) :

Pullback a LeftDistribClass instance along an injective function.

theorem Function.Injective.rightDistribClass {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Mul α] [Add α] [RightDistribClass α] (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) :

Pullback a RightDistribClass instance along an injective function.

@[reducible, inline]
abbrev Function.Injective.distrib {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Distrib α] (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y) :

Pullback a Distrib instance along an injective function.

Equations
Instances For
    @[reducible, inline]
    abbrev Function.Injective.hasDistribNeg {α : Type u_1} {β : Type u_2} [Mul β] [Neg β] (f : βα) (hf : Function.Injective f) [Mul α] [HasDistribNeg α] (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
    Instances For
      @[reducible, inline]
      abbrev Function.Injective.nonUnitalNonAssocSemiring {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Zero β] [SMul β] [NonUnitalNonAssocSemiring α] (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 : ∀ (n : ) (x : β), f (n x) = n f x) :

      Pullback a NonUnitalNonAssocSemiring instance along an injective function.

      Equations
      Instances For
        @[reducible, inline]
        abbrev Function.Injective.nonUnitalSemiring {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Zero β] [SMul β] [NonUnitalSemiring α] (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 : ∀ (n : ) (x : β), f (n x) = n f x) :

        Pullback a NonUnitalSemiring instance along an injective function.

        Equations
        Instances For
          @[reducible, inline]
          abbrev Function.Injective.nonAssocSemiring {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Zero β] [One β] [SMul β] [NatCast β] [NonAssocSemiring α] (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) (natCast : ∀ (n : ), f n = n) :

          Pullback a NonAssocSemiring instance along an injective function.

          Equations
          Instances For
            @[reducible, inline]
            abbrev Function.Injective.semiring {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Zero β] [One β] [SMul β] [Pow β ] [NatCast β] [Semiring α] (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 Semiring instance along an injective function.

            Equations
            Instances For
              @[reducible, inline]
              abbrev Function.Injective.nonUnitalNonAssocRing {α : Type u_1} {β : Type u_2} [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul β] [SMul β] [NonUnitalNonAssocRing α] (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 : ∀ (n : ) (x : β), f (n x) = n f x) (zsmul : ∀ (n : ) (x : β), f (n x) = n f x) :

              Pullback a NonUnitalNonAssocRing instance along an injective function.

              Equations
              Instances For
                @[reducible, inline]
                abbrev Function.Injective.nonUnitalRing {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul β] [SMul β] [NonUnitalRing α] (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 : ∀ (n : ) (x : β), f (n x) = n f x) (zsmul : ∀ (n : ) (x : β), f (n x) = n f x) :

                Pullback a NonUnitalRing instance along an injective function.

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev Function.Injective.nonAssocRing {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul β] [SMul β] [NatCast β] [IntCast β] [NonAssocRing α] (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) (natCast : ∀ (n : ), f n = n) (intCast : ∀ (n : ), f n = n) :

                  Pullback a NonAssocRing instance along an injective function.

                  Equations
                  Instances For
                    @[reducible, inline]
                    abbrev Function.Injective.ring {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] [Ring α] (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) :
                    Ring β

                    Pullback a Ring instance along an injective function.

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev Function.Injective.nonUnitalNonAssocCommSemiring {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Zero β] [SMul β] [NonUnitalNonAssocCommSemiring α] (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 : ∀ (n : ) (x : β), f (n x) = n f x) :

                      Pullback a NonUnitalNonAssocCommSemiring instance along an injective function.

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev Function.Injective.nonUnitalCommSemiring {α : Type u_1} {β : Type u_2} [Add β] [Mul β] [Zero β] [SMul β] [NonUnitalCommSemiring α] (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 : ∀ (n : ) (x : β), f (n x) = n f x) :

                        Pullback a NonUnitalCommSemiring instance along an injective function.

                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev Function.Injective.commSemiring {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Zero β] [One β] [SMul β] [Pow β ] [NatCast β] [CommSemiring α] (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 CommSemiring instance along an injective function.

                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev Function.Injective.nonUnitalNonAssocCommRing {α : Type u_1} {β : Type u_2} [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul β] [SMul β] [NonUnitalNonAssocCommRing α] (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 : ∀ (n : ) (x : β), f (n x) = n f x) (zsmul : ∀ (n : ) (x : β), f (n x) = n f x) :

                            Pullback a NonUnitalNonAssocCommRing instance along an injective function.

                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev Function.Injective.nonUnitalCommRing {α : Type u_1} {β : Type u_2} [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul β] [SMul β] [NonUnitalCommRing α] (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 : ∀ (n : ) (x : β), f (n x) = n f x) (zsmul : ∀ (n : ) (x : β), f (n x) = n f x) :

                              Pullback a NonUnitalCommRing instance along an injective function.

                              Equations
                              Instances For
                                @[reducible, inline]
                                abbrev Function.Injective.commRing {α : Type u_1} {β : Type u_2} (f : βα) (hf : Function.Injective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] [CommRing α] (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 CommRing instance along an injective function.

                                Equations
                                Instances For
                                  theorem Function.Surjective.leftDistribClass {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Mul α] [Add α] [LeftDistribClass α] (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) :

                                  Pushforward a LeftDistribClass instance along a surjective function.

                                  theorem Function.Surjective.rightDistribClass {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Mul α] [Add α] [RightDistribClass α] (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) :

                                  Pushforward a RightDistribClass instance along a surjective function.

                                  @[reducible, inline]
                                  abbrev Function.Surjective.distrib {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Distrib α] (add : ∀ (x y : α), f (x + y) = f x + f y) (mul : ∀ (x y : α), f (x * y) = f x * f y) :

                                  Pushforward a Distrib instance along a surjective function.

                                  Equations
                                  Instances For
                                    @[reducible, inline]
                                    abbrev Function.Surjective.hasDistribNeg {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Mul β] [Neg β] [Mul α] [HasDistribNeg α] (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
                                    Instances For
                                      @[reducible, inline]
                                      abbrev Function.Surjective.nonUnitalNonAssocSemiring {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [SMul β] [NonUnitalNonAssocSemiring α] (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 : ∀ (n : ) (x : α), f (n x) = n f x) :

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

                                      Equations
                                      Instances For
                                        @[reducible, inline]
                                        abbrev Function.Surjective.nonUnitalSemiring {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [SMul β] [NonUnitalSemiring α] (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 : ∀ (n : ) (x : α), f (n x) = n f x) :

                                        Pushforward a NonUnitalSemiring instance along a surjective function.

                                        Equations
                                        Instances For
                                          @[reducible, inline]
                                          abbrev Function.Surjective.nonAssocSemiring {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [One β] [SMul β] [NatCast β] [NonAssocSemiring α] (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) (natCast : ∀ (n : ), f n = n) :

                                          Pushforward a NonAssocSemiring instance along a surjective function.

                                          Equations
                                          Instances For
                                            @[reducible, inline]
                                            abbrev Function.Surjective.semiring {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [One β] [SMul β] [Pow β ] [NatCast β] [Semiring α] (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) :

                                            Pushforward a Semiring instance along a surjective function.

                                            Equations
                                            Instances For
                                              @[reducible, inline]
                                              abbrev Function.Surjective.nonUnitalNonAssocRing {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul β] [SMul β] [NonUnitalNonAssocRing α] (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 : ∀ (n : ) (x : α), f (n x) = n f x) (zsmul : ∀ (n : ) (x : α), f (n x) = n f x) :

                                              Pushforward a NonUnitalNonAssocRing instance along a surjective function.

                                              Equations
                                              Instances For
                                                @[reducible, inline]
                                                abbrev Function.Surjective.nonUnitalRing {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul β] [SMul β] [NonUnitalRing α] (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 : ∀ (n : ) (x : α), f (n x) = n f x) (zsmul : ∀ (n : ) (x : α), f (n x) = n f x) :

                                                Pushforward a NonUnitalRing instance along a surjective function.

                                                Equations
                                                Instances For
                                                  @[reducible, inline]
                                                  abbrev Function.Surjective.nonAssocRing {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul β] [SMul β] [NatCast β] [IntCast β] [NonAssocRing α] (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) (natCast : ∀ (n : ), f n = n) (intCast : ∀ (n : ), f n = n) :

                                                  Pushforward a NonAssocRing instance along a surjective function.

                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]
                                                    abbrev Function.Surjective.ring {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] [Ring α] (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) :
                                                    Ring β

                                                    Pushforward a Ring instance along a surjective function.

                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      abbrev Function.Surjective.nonUnitalNonAssocCommSemiring {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [SMul β] [NonUnitalNonAssocCommSemiring α] (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 : ∀ (n : ) (x : α), f (n x) = n f x) :

                                                      Pushforward a NonUnitalNonAssocCommSemiring instance along a surjective function.

                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        abbrev Function.Surjective.nonUnitalCommSemiring {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [SMul β] [NonUnitalCommSemiring α] (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 : ∀ (n : ) (x : α), f (n x) = n f x) :

                                                        Pushforward a NonUnitalCommSemiring instance along a surjective function.

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev Function.Surjective.commSemiring {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [One β] [SMul β] [Pow β ] [NatCast β] [CommSemiring α] (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) :

                                                          Pushforward a CommSemiring instance along a surjective function.

                                                          Equations
                                                          Instances For
                                                            @[reducible, inline]
                                                            abbrev Function.Surjective.nonUnitalNonAssocCommRing {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul β] [SMul β] [NonUnitalNonAssocCommRing α] (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 : ∀ (n : ) (x : α), f (n x) = n f x) (zsmul : ∀ (n : ) (x : α), f (n x) = n f x) :

                                                            Pushforward a NonUnitalNonAssocCommRing instance along a surjective function.

                                                            Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              abbrev Function.Surjective.nonUnitalCommRing {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [Neg β] [Sub β] [SMul β] [SMul β] [NonUnitalCommRing α] (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 : ∀ (n : ) (x : α), f (n x) = n f x) (zsmul : ∀ (n : ) (x : α), f (n x) = n f x) :

                                                              Pushforward a NonUnitalCommRing instance along a surjective function.

                                                              Equations
                                                              Instances For
                                                                @[reducible, inline]
                                                                abbrev Function.Surjective.commRing {α : Type u_1} {β : Type u_2} (f : αβ) (hf : Function.Surjective f) [Add β] [Mul β] [Zero β] [One β] [Neg β] [Sub β] [SMul β] [SMul β] [Pow β ] [NatCast β] [IntCast β] [CommRing α] (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) :

                                                                Pushforward a CommRing instance along a surjective function.

                                                                Equations
                                                                Instances For
                                                                  Equations