Documentation

Mathlib.Algebra.Group.InjSurj

Lifting algebraic data classes along injective/surjective maps #

This file provides definitions that are meant to deal with situations such as the following:

Suppose that G is a group, and H is a type endowed with One H, Mul H, and Inv H. Suppose furthermore, that f : G → H is a surjective map that respects the multiplication, and the unit elements. Then H satisfies the group axioms.

The relevant definition in this case is Function.Surjective.group. Dually, there is also Function.Injective.group. And there are versions for (additive) (commutative) semigroups/monoids.

Injective #

theorem Function.Injective.addSemigroup.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) (y : M₁) (z : M₁) :
x + y + z = x + (y + z)
@[reducible]
def Function.Injective.addSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) :

A type endowed with + is an additive semigroup, if it admits an injective map that preserves + to an additive semigroup.

Equations
Instances For
    @[reducible]
    def Function.Injective.semigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [Semigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) :

    A type endowed with * is a semigroup, if it admits an injective map that preserves * to a semigroup. See note [reducible non-instances].

    Equations
    Instances For
      @[reducible]
      def Function.Injective.addCommSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddCommSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) :

      A type endowed with + is an additive commutative semigroup,if it admits an injective map that preserves + to an additive commutative semigroup.

      Equations
      Instances For
        theorem Function.Injective.addCommSemigroup.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddCommSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) (y : M₁) :
        x + y = y + x
        @[reducible]
        def Function.Injective.commSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [CommSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) :

        A type endowed with * is a commutative semigroup, if it admits an injective map that preserves * to a commutative semigroup. See note [reducible non-instances].

        Equations
        Instances For
          @[reducible]
          def Function.Injective.addLeftCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddLeftCancelSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) :

          A type endowed with + is an additive left cancel semigroup, if it admits an injective map that preserves + to an additive left cancel semigroup.

          Equations
          Instances For
            theorem Function.Injective.addLeftCancelSemigroup.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddLeftCancelSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) (y : M₁) (z : M₁) (H : x + y = x + z) :
            y = z
            @[reducible]
            def Function.Injective.leftCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [LeftCancelSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) :

            A type endowed with * is a left cancel semigroup, if it admits an injective map that preserves * to a left cancel semigroup. See note [reducible non-instances].

            Equations
            Instances For
              @[reducible]
              def Function.Injective.addRightCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddRightCancelSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) :

              A type endowed with + is an additive right cancel semigroup, if it admits an injective map that preserves + to an additive right cancel semigroup.

              Equations
              Instances For
                theorem Function.Injective.addRightCancelSemigroup.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [AddRightCancelSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) (y : M₁) (z : M₁) (H : x + y = z + y) :
                x = z
                @[reducible]
                def Function.Injective.rightCancelSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [RightCancelSemigroup M₂] (f : M₁M₂) (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) :

                A type endowed with * is a right cancel semigroup, if it admits an injective map that preserves * to a right cancel semigroup. See note [reducible non-instances].

                Equations
                Instances For
                  theorem Function.Injective.addZeroClass.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [AddZeroClass M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) :
                  x + 0 = x
                  @[reducible]
                  def Function.Injective.addZeroClass {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [AddZeroClass M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) :

                  A type endowed with 0 and + is an AddZeroClass, if it admits an injective map that preserves 0 and + to an AddZeroClass.

                  Equations
                  Instances For
                    theorem Function.Injective.addZeroClass.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [AddZeroClass M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (x : M₁) :
                    0 + x = x
                    @[reducible]
                    def Function.Injective.mulOneClass {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [MulOneClass M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) :

                    A type endowed with 1 and * is a MulOneClass, if it admits an injective map that preserves 1 and * to a MulOneClass. See note [reducible non-instances].

                    Equations
                    Instances For
                      @[reducible]
                      def Function.Injective.addMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                      A type endowed with 0 and + is an additive monoid, if it admits an injective map that preserves 0 and + to an additive monoid. See note [reducible non-instances].

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem Function.Injective.addMonoid.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (x : M₁) :
                        (fun n x => n x) 0 x = 0
                        theorem Function.Injective.addMonoid.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (n : ) (x : M₁) :
                        (fun n x => n x) (n + 1) x = x + (fun n x => n x) n x
                        @[reducible]
                        def Function.Injective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [Monoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :
                        Monoid M₁

                        A type endowed with 1 and * is a monoid, if it admits an injective map that preserves 1 and * to a monoid. See note [reducible non-instances].

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[reducible]
                          def Function.Injective.addMonoidWithOne {M₂ : Type u_2} {M₁ : Type u_3} [Zero M₁] [One M₁] [Add M₁] [SMul M₁] [NatCast M₁] [AddMonoidWithOne M₂] (f : M₁M₂) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) :

                          A type endowed with 0, 1 and + is an additive monoid with one, if it admits an injective map that preserves 0, 1 and + to an additive monoid with one. See note [reducible non-instances].

                          Equations
                          Instances For
                            @[reducible]
                            def Function.Injective.addLeftCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddLeftCancelMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                            A type endowed with 0 and + is an additive left cancel monoid, if it admits an injective map that preserves 0 and + to an additive left cancel monoid.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[reducible]
                              def Function.Injective.leftCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [LeftCancelMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                              A type endowed with 1 and * is a left cancel monoid, if it admits an injective map that preserves 1 and * to a left cancel monoid. See note [reducible non-instances].

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[reducible]
                                def Function.Injective.addRightCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddRightCancelMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                A type endowed with 0 and + is an additive left cancel monoid,if it admits an injective map that preserves 0 and + to an additive left cancel monoid.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[reducible]
                                  def Function.Injective.rightCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [RightCancelMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                  A type endowed with 1 and * is a right cancel monoid, if it admits an injective map that preserves 1 and * to a right cancel monoid. See note [reducible non-instances].

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[reducible]
                                    def Function.Injective.addCancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddCancelMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                    A type endowed with 0 and + is an additive left cancel monoid,if it admits an injective map that preserves 0 and + to an additive left cancel monoid.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem Function.Injective.addCancelMonoid.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddCancelMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (a : M₁) (b : M₁) (c : M₁) :
                                      a + b = c + ba = c
                                      @[reducible]
                                      def Function.Injective.cancelMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [CancelMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                      A type endowed with 1 and * is a cancel monoid, if it admits an injective map that preserves 1 and * to a cancel monoid. See note [reducible non-instances].

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[reducible]
                                        def Function.Injective.addCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddCommMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                        A type endowed with 0 and + is an additive commutative monoid, if it admits an injective map that preserves 0 and + to an additive commutative monoid.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[reducible]
                                          def Function.Injective.commMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [CommMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                          A type endowed with 1 and * is a commutative monoid, if it admits an injective map that preserves 1 and * to a commutative monoid. See note [reducible non-instances].

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[reducible]
                                            def Function.Injective.addCommMonoidWithOne {M₂ : Type u_2} {M₁ : Type u_3} [Zero M₁] [One M₁] [Add M₁] [SMul M₁] [NatCast M₁] [AddCommMonoidWithOne M₂] (f : M₁M₂) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) :

                                            A type endowed with 0, 1 and + is an additive commutative monoid with one, if it admits an injective map that preserves 0, 1 and + to an additive commutative monoid with one. See note [reducible non-instances].

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem Function.Injective.addCancelCommMonoid.proof_3 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddCancelCommMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (x : M₁) :
                                              @[reducible]
                                              def Function.Injective.addCancelCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddCancelCommMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                              A type endowed with 0 and + is an additive cancel commutative monoid, if it admits an injective map that preserves 0 and + to an additive cancel commutative monoid.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem Function.Injective.addCancelCommMonoid.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddCancelCommMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (a : M₁) :
                                                a + 0 = a
                                                theorem Function.Injective.addCancelCommMonoid.proof_4 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddCancelCommMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (n : ) (x : M₁) :
                                                theorem Function.Injective.addCancelCommMonoid.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [AddCancelCommMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (a : M₁) :
                                                0 + a = a
                                                @[reducible]
                                                def Function.Injective.cancelCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [CancelCommMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                                A type endowed with 1 and * is a cancel commutative monoid, if it admits an injective map that preserves 1 and * to a cancel commutative monoid. See note [reducible non-instances].

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[reducible]
                                                  def Function.Injective.involutiveNeg {M₂ : Type u_2} {M₁ : Type u_3} [Neg M₁] [InvolutiveNeg M₂] (f : M₁M₂) (hf : Function.Injective f) (inv : ∀ (x : M₁), f (-x) = -f x) :

                                                  A type has an involutive negation if it admits a surjective map that preserves - to a type which has an involutive negation.

                                                  Equations
                                                  Instances For
                                                    theorem Function.Injective.involutiveNeg.proof_1 {M₂ : Type u_2} {M₁ : Type u_1} [Neg M₁] [InvolutiveNeg M₂] (f : M₁M₂) (hf : Function.Injective f) (inv : ∀ (x : M₁), f (-x) = -f x) (x : M₁) :
                                                    - -x = x
                                                    @[reducible]
                                                    def Function.Injective.involutiveInv {M₂ : Type u_2} {M₁ : Type u_3} [Inv M₁] [InvolutiveInv M₂] (f : M₁M₂) (hf : Function.Injective f) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) :

                                                    A type has an involutive inversion if it admits a surjective map that preserves ⁻¹ to a type which has an involutive inversion. See note [reducible non-instances]

                                                    Equations
                                                    Instances For
                                                      theorem Function.Injective.negZeroClass.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Zero M₁] [Neg M₁] [NegZeroClass M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (inv : ∀ (x : M₁), f (-x) = -f x) :
                                                      -0 = 0
                                                      @[reducible]
                                                      def Function.Injective.negZeroClass {M₁ : Type u_1} {M₂ : Type u_2} [Zero M₁] [Neg M₁] [NegZeroClass M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (inv : ∀ (x : M₁), f (-x) = -f x) :

                                                      A type endowed with 0 and unary - is an NegZeroClass, if it admits an injective map that preserves 0 and unary - to an NegZeroClass.

                                                      Equations
                                                      Instances For
                                                        @[reducible]
                                                        def Function.Injective.invOneClass {M₁ : Type u_1} {M₂ : Type u_2} [One M₁] [Inv M₁] [InvOneClass M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) :

                                                        A type endowed with 1 and ⁻¹ is a InvOneClass, if it admits an injective map that preserves 1 and ⁻¹ to a InvOneClass. See note [reducible non-instances].

                                                        Equations
                                                        Instances For
                                                          theorem Function.Injective.subNegMonoid.proof_3 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [SMul M₁] [SubNegMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) (n : ) (x : M₁) :
                                                          (fun n x => n x) (Int.ofNat (Nat.succ n)) x = x + (fun n x => n x) (Int.ofNat n) x
                                                          theorem Function.Injective.subNegMonoid.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SubNegMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (x : M₁) (y : M₁) :
                                                          x - y = x + -y
                                                          @[reducible]
                                                          def Function.Injective.subNegMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [SubNegMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                          A type endowed with 0, +, unary -, and binary - is a SubNegMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubNegMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            theorem Function.Injective.subNegMonoid.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [SMul M₁] [SubNegMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) (x : M₁) :
                                                            (fun n x => n x) 0 x = 0
                                                            theorem Function.Injective.subNegMonoid.proof_4 {M₁ : Type u_1} {M₂ : Type u_2} [Neg M₁] [SMul M₁] [SubNegMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (inv : ∀ (x : M₁), f (-x) = -f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) (n : ) (x : M₁) :
                                                            (fun n x => n x) (Int.negSucc n) x = -(fun n x => n x) (↑(Nat.succ n)) x
                                                            @[reducible]
                                                            def Function.Injective.divInvMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [Inv M₁] [Div M₁] [Pow M₁ ] [DivInvMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                                            A type endowed with 1, *, ⁻¹, and / is a DivInvMonoid if it admits an injective map that preserves 1, *, ⁻¹, and / to a DivInvMonoid. See note [reducible non-instances].

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[reducible]
                                                              def Function.Injective.subNegZeroMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [SubNegZeroMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                              A type endowed with 0, +, unary -, and binary - is a SubNegZeroMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubNegZeroMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[reducible]
                                                                def Function.Injective.divInvOneMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [Inv M₁] [Div M₁] [Pow M₁ ] [DivInvOneMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                                                A type endowed with 1, *, ⁻¹, and / is a DivInvOneMonoid if it admits an injective map that preserves 1, *, ⁻¹, and / to a DivInvOneMonoid. See note [reducible non-instances].

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  theorem Function.Injective.subtractionMonoid.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [SubtractionMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) (x : M₁) (y : M₁) :
                                                                  -(x + y) = -y + -x
                                                                  @[reducible]
                                                                  def Function.Injective.subtractionMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [SubtractionMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                                  A type endowed with 0, +, unary -, and binary - is a SubtractionMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubtractionMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    theorem Function.Injective.subtractionMonoid.proof_2 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [SubtractionMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) (x : M₁) (y : M₁) (h : x + y = 0) :
                                                                    -x = y
                                                                    @[reducible]
                                                                    def Function.Injective.divisionMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [Inv M₁] [Div M₁] [Pow M₁ ] [DivisionMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                                                    A type endowed with 1, *, ⁻¹, and / is a DivisionMonoid if it admits an injective map that preserves 1, *, ⁻¹, and / to a DivisionMonoid. See note [reducible non-instances]

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      @[reducible]
                                                                      def Function.Injective.subtractionCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [SubtractionCommMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                                      A type endowed with 0, +, unary -, and binary - is a SubtractionCommMonoid if it admits an injective map that preserves 0, +, unary -, and binary - to a SubtractionCommMonoid. This version takes custom nsmul and zsmul as [SMul ℕ M₁] and [SMul ℤ M₁] arguments.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        @[reducible]
                                                                        def Function.Injective.divisionCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [Inv M₁] [Div M₁] [Pow M₁ ] [DivisionCommMonoid M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                                                        A type endowed with 1, *, ⁻¹, and / is a DivisionCommMonoid if it admits an injective map that preserves 1, *, ⁻¹, and / to a DivisionCommMonoid. See note [reducible non-instances].

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[reducible]
                                                                          def Function.Injective.addGroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [AddGroup M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                                          A type endowed with 0 and + is an additive group, if it admits an injective map that preserves 0 and + to an additive group.

                                                                          Equations
                                                                          Instances For
                                                                            theorem Function.Injective.addGroup.proof_1 {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [AddGroup M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) (x : M₁) :
                                                                            -x + x = 0
                                                                            @[reducible]
                                                                            def Function.Injective.group {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [Inv M₁] [Div M₁] [Pow M₁ ] [Group M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :
                                                                            Group M₁

                                                                            A type endowed with 1, * and ⁻¹ is a group, if it admits an injective map that preserves 1, * and ⁻¹ to a group. See note [reducible non-instances].

                                                                            Equations
                                                                            Instances For
                                                                              @[reducible]
                                                                              def Function.Injective.addGroupWithOne {M₂ : Type u_2} {M₁ : Type u_3} [Zero M₁] [One M₁] [Add M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [NatCast M₁] [IntCast M₁] [AddGroupWithOne M₂] (f : M₁M₂) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (neg : ∀ (x : M₁), f (-x) = -f x) (sub : ∀ (x y : M₁), f (x - y) = f x - f y) (nsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (zsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

                                                                              A type endowed with 0, 1 and + is an additive group with one, if it admits an injective map that preserves 0, 1 and + to an additive group with one. See note [reducible non-instances].

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                @[reducible]
                                                                                def Function.Injective.addCommGroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₁] [Zero M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [AddCommGroup M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                                                A type endowed with 0 and + is an additive commutative group, if it admits an injective map that preserves 0 and + to an additive commutative group.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  @[reducible]
                                                                                  def Function.Injective.commGroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₁] [One M₁] [Pow M₁ ] [Inv M₁] [Div M₁] [Pow M₁ ] [CommGroup M₂] (f : M₁M₂) (hf : Function.Injective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                                                                  A type endowed with 1, * and ⁻¹ is a commutative group, if it admits an injective map that preserves 1, * and ⁻¹ to a commutative group. See note [reducible non-instances].

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[reducible]
                                                                                    def Function.Injective.addCommGroupWithOne {M₂ : Type u_2} {M₁ : Type u_3} [Zero M₁] [One M₁] [Add M₁] [SMul M₁] [Neg M₁] [Sub M₁] [SMul M₁] [NatCast M₁] [IntCast M₁] [AddCommGroupWithOne M₂] (f : M₁M₂) (hf : Function.Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (neg : ∀ (x : M₁), f (-x) = -f x) (sub : ∀ (x y : M₁), f (x - y) = f x - f y) (nsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (zsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

                                                                                    A type endowed with 0, 1 and + is an additive commutative group with one, if it admits an injective map that preserves 0, 1 and + to an additive commutative group with one. See note [reducible non-instances].

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

                                                                                      Surjective #

                                                                                      @[reducible]
                                                                                      def Function.Surjective.addSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [AddSemigroup M₁] (f : M₁M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) :

                                                                                      A type endowed with + is an additive semigroup, if it admits a surjective map that preserves + from an additive semigroup.

                                                                                      Equations
                                                                                      Instances For
                                                                                        theorem Function.Surjective.addSemigroup.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [Add M₂] [AddSemigroup M₁] (f : M₁M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (y₁ : M₂) (y₂ : M₂) (y₃ : M₂) :
                                                                                        y₁ + y₂ + y₃ = y₁ + (y₂ + y₃)
                                                                                        @[reducible]
                                                                                        def Function.Surjective.semigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [Semigroup M₁] (f : M₁M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) :

                                                                                        A type endowed with * is a semigroup, if it admits a surjective map that preserves * from a semigroup. See note [reducible non-instances].

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[reducible]
                                                                                          def Function.Surjective.addCommSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [AddCommSemigroup M₁] (f : M₁M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) :

                                                                                          A type endowed with + is an additive commutative semigroup, if it admits a surjective map that preserves + from an additive commutative semigroup.

                                                                                          Equations
                                                                                          Instances For
                                                                                            theorem Function.Surjective.addCommSemigroup.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [Add M₂] [AddCommSemigroup M₁] (f : M₁M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (y₁ : M₂) (y₂ : M₂) :
                                                                                            y₁ + y₂ = y₂ + y₁
                                                                                            @[reducible]
                                                                                            def Function.Surjective.commSemigroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [CommSemigroup M₁] (f : M₁M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) :

                                                                                            A type endowed with * is a commutative semigroup, if it admits a surjective map that preserves * from a commutative semigroup. See note [reducible non-instances].

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[reducible]
                                                                                              def Function.Surjective.addZeroClass {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [AddZeroClass M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) :

                                                                                              A type endowed with 0 and + is an AddZeroClass, if it admits a surjective map that preserves 0 and + to an AddZeroClass.

                                                                                              Equations
                                                                                              Instances For
                                                                                                theorem Function.Surjective.addZeroClass.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [Add M₂] [Zero M₂] [AddZeroClass M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (y : M₂) :
                                                                                                0 + y = y
                                                                                                theorem Function.Surjective.addZeroClass.proof_2 {M₁ : Type u_2} {M₂ : Type u_1} [Add M₂] [Zero M₂] [AddZeroClass M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (y : M₂) :
                                                                                                y + 0 = y
                                                                                                @[reducible]
                                                                                                def Function.Surjective.mulOneClass {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [MulOneClass M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) :

                                                                                                A type endowed with 1 and * is a MulOneClass, if it admits a surjective map that preserves 1 and * from a MulOneClass. See note [reducible non-instances].

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[reducible]
                                                                                                  def Function.Surjective.addMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [SMul M₂] [AddMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                                                                  A type endowed with 0 and + is an additive monoid, if it admits a surjective map that preserves 0 and + to an additive monoid. This version takes a custom nsmul as a [SMul ℕ M₂] argument.

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    theorem Function.Surjective.addMonoid.proof_2 {M₁ : Type u_2} {M₂ : Type u_1} [Add M₂] [SMul M₂] [AddMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (n : ) (y : M₂) :
                                                                                                    (fun n x => n x) (n + 1) y = y + (fun n x => n x) n y
                                                                                                    theorem Function.Surjective.addMonoid.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [Add M₂] [Zero M₂] [SMul M₂] [AddMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (y : M₂) :
                                                                                                    (fun n x => n x) 0 y = 0
                                                                                                    @[reducible]
                                                                                                    def Function.Surjective.monoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [Pow M₂ ] [Monoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :
                                                                                                    Monoid M₂

                                                                                                    A type endowed with 1 and * is a monoid, if it admits a surjective map that preserves 1 and * to a monoid. See note [reducible non-instances].

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      @[reducible]
                                                                                                      def Function.Surjective.addMonoidWithOne {M₁ : Type u_1} {M₂ : Type u_3} [Zero M₂] [One M₂] [Add M₂] [SMul M₂] [NatCast M₂] [AddMonoidWithOne M₁] (f : M₁M₂) (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) :

                                                                                                      A type endowed with 0, 1 and + is an additive monoid with one, if it admits a surjective map that preserves 0, 1 and * from an additive monoid with one. See note [reducible non-instances].

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[reducible]
                                                                                                        def Function.Surjective.addCommMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [SMul M₂] [AddCommMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                                                                        A type endowed with 0 and + is an additive commutative monoid, if it admits a surjective map that preserves 0 and + to an additive commutative monoid.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          @[reducible]
                                                                                                          def Function.Surjective.commMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [Pow M₂ ] [CommMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                                                                                          A type endowed with 1 and * is a commutative monoid, if it admits a surjective map that preserves 1 and * from a commutative monoid. See note [reducible non-instances].

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            @[reducible]
                                                                                                            def Function.Surjective.addCommMonoidWithOne {M₁ : Type u_1} {M₂ : Type u_3} [Zero M₂] [One M₂] [Add M₂] [SMul M₂] [NatCast M₂] [AddCommMonoidWithOne M₁] (f : M₁M₂) (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (nsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) :

                                                                                                            A type endowed with 0, 1 and + is an additive monoid with one, if it admits a surjective map that preserves 0, 1 and * from an additive monoid with one. See note [reducible non-instances].

                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              theorem Function.Surjective.involutiveNeg.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [Neg M₂] [InvolutiveNeg M₁] (f : M₁M₂) (hf : Function.Surjective f) (inv : ∀ (x : M₁), f (-x) = -f x) (y : M₂) :
                                                                                                              - -y = y
                                                                                                              @[reducible]
                                                                                                              def Function.Surjective.involutiveNeg {M₁ : Type u_1} {M₂ : Type u_3} [Neg M₂] [InvolutiveNeg M₁] (f : M₁M₂) (hf : Function.Surjective f) (inv : ∀ (x : M₁), f (-x) = -f x) :

                                                                                                              A type has an involutive negation if it admits a surjective map that preserves - to a type which has an involutive negation.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[reducible]
                                                                                                                def Function.Surjective.involutiveInv {M₁ : Type u_1} {M₂ : Type u_3} [Inv M₂] [InvolutiveInv M₁] (f : M₁M₂) (hf : Function.Surjective f) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) :

                                                                                                                A type has an involutive inversion if it admits a surjective map that preserves ⁻¹ to a type which has an involutive inversion. See note [reducible non-instances]

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  theorem Function.Surjective.subNegMonoid.proof_3 {M₁ : Type u_2} {M₂ : Type u_1} [Add M₂] [Zero M₂] [SMul M₂] [SMul M₂] [SubNegMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) (n : ) (y : M₂) :
                                                                                                                  (fun n x => n x) (Int.ofNat (Nat.succ n)) y = y + (fun n x => n x) (Int.ofNat n) y
                                                                                                                  theorem Function.Surjective.subNegMonoid.proof_2 {M₁ : Type u_2} {M₂ : Type u_1} [Add M₂] [Zero M₂] [SMul M₂] [SMul M₂] [SubNegMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) (y : M₂) :
                                                                                                                  (fun n x => n x) 0 y = 0
                                                                                                                  theorem Function.Surjective.subNegMonoid.proof_4 {M₁ : Type u_2} {M₂ : Type u_1} [Neg M₂] [SMul M₂] [SubNegMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (inv : ∀ (x : M₁), f (-x) = -f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) (n : ) (y : M₂) :
                                                                                                                  (fun n x => n x) (Int.negSucc n) y = -(fun n x => n x) (↑(Nat.succ n)) y
                                                                                                                  @[reducible]
                                                                                                                  def Function.Surjective.subNegMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [SMul M₂] [Neg M₂] [Sub M₂] [SMul M₂] [SubNegMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                                                                                  A type endowed with 0, +, unary -, and binary - is a SubNegMonoid if it admits a surjective map that preserves 0, +, unary -, and binary - to a SubNegMonoid.

                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For
                                                                                                                    theorem Function.Surjective.subNegMonoid.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [Add M₂] [Zero M₂] [SMul M₂] [Neg M₂] [Sub M₂] [SubNegMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (y₁ : M₂) (y₂ : M₂) :
                                                                                                                    y₁ - y₂ = y₁ + -y₂
                                                                                                                    @[reducible]
                                                                                                                    def Function.Surjective.divInvMonoid {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [Pow M₂ ] [Inv M₂] [Div M₂] [Pow M₂ ] [DivInvMonoid M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                                                                                                    A type endowed with 1, *, ⁻¹, and / is a DivInvMonoid if it admits a surjective map that preserves 1, *, ⁻¹, and / to a DivInvMonoid. See note [reducible non-instances].

                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      theorem Function.Surjective.addGroup.proof_1 {M₁ : Type u_2} {M₂ : Type u_1} [Add M₂] [Zero M₂] [SMul M₂] [Neg M₂] [Sub M₂] [SMul M₂] [AddGroup M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) (y : M₂) :
                                                                                                                      -y + y = 0
                                                                                                                      @[reducible]
                                                                                                                      def Function.Surjective.addGroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [SMul M₂] [Neg M₂] [Sub M₂] [SMul M₂] [AddGroup M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                                                                                      A type endowed with 0 and + is an additive group, if it admits a surjective map that preserves 0 and + to an additive group.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[reducible]
                                                                                                                        def Function.Surjective.group {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [Pow M₂ ] [Inv M₂] [Div M₂] [Pow M₂ ] [Group M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :
                                                                                                                        Group M₂

                                                                                                                        A type endowed with 1, * and ⁻¹ is a group, if it admits a surjective map that preserves 1, * and ⁻¹ to a group. See note [reducible non-instances].

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[reducible]
                                                                                                                          def Function.Surjective.addGroupWithOne {M₁ : Type u_1} {M₂ : Type u_3} [Zero M₂] [One M₂] [Add M₂] [Neg M₂] [Sub M₂] [SMul M₂] [SMul M₂] [NatCast M₂] [IntCast M₂] [AddGroupWithOne M₁] (f : M₁M₂) (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (neg : ∀ (x : M₁), f (-x) = -f x) (sub : ∀ (x y : M₁), f (x - y) = f x - f y) (nsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (zsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

                                                                                                                          A type endowed with 0, 1, + is an additive group with one, if it admits a surjective map that preserves 0, 1, and + to an additive group with one. See note [reducible non-instances].

                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For
                                                                                                                            @[reducible]
                                                                                                                            def Function.Surjective.addCommGroup {M₁ : Type u_1} {M₂ : Type u_2} [Add M₂] [Zero M₂] [SMul M₂] [Neg M₂] [Sub M₂] [SMul M₂] [AddCommGroup M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x) (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ), f (n x) = n f x) (zpow : ∀ (x : M₁) (n : ), f (n x) = n f x) :

                                                                                                                            A type endowed with 0 and + is an additive commutative group, if it admits a surjective map that preserves 0 and + to an additive commutative group.

                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For
                                                                                                                              @[reducible]
                                                                                                                              def Function.Surjective.commGroup {M₁ : Type u_1} {M₂ : Type u_2} [Mul M₂] [One M₂] [Pow M₂ ] [Inv M₂] [Div M₂] [Pow M₂ ] [CommGroup M₁] (f : M₁M₂) (hf : Function.Surjective f) (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : M₁) (n : ), f (x ^ n) = f x ^ n) :

                                                                                                                              A type endowed with 1, *, ⁻¹, and / is a commutative group, if it admits a surjective map that preserves 1, *, ⁻¹, and / from a commutative group. See note [reducible non-instances].

                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                @[reducible]
                                                                                                                                def Function.Surjective.addCommGroupWithOne {M₁ : Type u_1} {M₂ : Type u_3} [Zero M₂] [One M₂] [Add M₂] [Neg M₂] [Sub M₂] [SMul M₂] [SMul M₂] [NatCast M₂] [IntCast M₂] [AddCommGroupWithOne M₁] (f : M₁M₂) (hf : Function.Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : M₁), f (x + y) = f x + f y) (neg : ∀ (x : M₁), f (-x) = -f x) (sub : ∀ (x y : M₁), f (x - y) = f x - f y) (nsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (zsmul : ∀ (x : M₁) (n : ), f (n x) = n f x) (nat_cast : ∀ (n : ), f n = n) (int_cast : ∀ (n : ), f n = n) :

                                                                                                                                A type endowed with 0, 1, + is an additive commutative group with one, if it admits a surjective map that preserves 0, 1, and + to an additive commutative group with one. See note [reducible non-instances].

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