Documentation

Mathlib.Algebra.Group.Hom.Defs

Monoid and group homomorphisms #

This file defines the bundled structures for monoid and group homomorphisms. Namely, we define MonoidHom (resp., AddMonoidHom) to be bundled homomorphisms between multiplicative (resp., additive) monoids or groups.

We also define coercion to a function, and usual operations: composition, identity homomorphism, pointwise multiplication and pointwise inversion.

This file also defines the lesser-used (and notation-less) homomorphism types which are used as building blocks for other homomorphisms:

Notations #

Implementation notes #

There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

There is no GroupHom -- the idea is that MonoidHom is used. The constructor for MonoidHom needs a proof of map_one as well as map_mul; a separate constructor MonoidHom.mk' will construct group homs (i.e. monoid homs between groups) given only a proof that multiplication is preserved,

Implicit {} brackets are often used instead of type class [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type MonoidHom. When they can be inferred from the type it is faster to use this method than to use type class inference.

Historically this file also included definitions of unbundled homomorphism classes; they were deprecated and moved to Deprecated/Group.

Tags #

MonoidHom, AddMonoidHom

structure ZeroHom (M : Type u_10) (N : Type u_11) [Zero M] [Zero N] :
Type (max u_10 u_11)

ZeroHom M N is the type of functions M → N that preserve zero.

When possible, instead of parametrizing results over (f : ZeroHom M N), you should parametrize over (F : Type*) [ZeroHomClass F M N] (f : F).

When you extend this structure, make sure to also extend ZeroHomClass.

  • toFun : MN

    The underlying function

  • map_zero' : self.toFun 0 = 0

    The proposition that the function preserves 0

Instances For
    theorem ZeroHom.map_zero' {M : Type u_10} {N : Type u_11} [Zero M] [Zero N] (self : ZeroHom M N) :
    self.toFun 0 = 0

    The proposition that the function preserves 0

    class ZeroHomClass (F : Type u_10) (M : outParam (Type u_11)) (N : outParam (Type u_12)) [Zero M] [Zero N] [FunLike F M N] :

    ZeroHomClass F M N states that F is a type of zero-preserving homomorphisms.

    You should extend this typeclass when you extend ZeroHom.

    • map_zero : ∀ (f : F), f 0 = 0

      The proposition that the function preserves 0

    Instances
      theorem ZeroHomClass.map_zero {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [Zero M] [Zero N] [FunLike F M N] [self : ZeroHomClass F M N] (f : F) :
      f 0 = 0

      The proposition that the function preserves 0

      structure AddHom (M : Type u_10) (N : Type u_11) [Add M] [Add N] :
      Type (max u_10 u_11)

      AddHom M N is the type of functions M → N that preserve addition.

      When possible, instead of parametrizing results over (f : AddHom M N), you should parametrize over (F : Type*) [AddHomClass F M N] (f : F).

      When you extend this structure, make sure to extend AddHomClass.

      • toFun : MN

        The underlying function

      • map_add' : ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y

        The proposition that the function preserves addition

      Instances For
        theorem AddHom.map_add' {M : Type u_10} {N : Type u_11} [Add M] [Add N] (self : AddHom M N) (x : M) (y : M) :
        self.toFun (x + y) = self.toFun x + self.toFun y

        The proposition that the function preserves addition

        class AddHomClass (F : Type u_10) (M : outParam (Type u_11)) (N : outParam (Type u_12)) [Add M] [Add N] [FunLike F M N] :

        AddHomClass F M N states that F is a type of addition-preserving homomorphisms. You should declare an instance of this typeclass when you extend AddHom.

        • map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y

          The proposition that the function preserves addition

        Instances
          theorem AddHomClass.map_add {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [Add M] [Add N] [FunLike F M N] [self : AddHomClass F M N] (f : F) (x : M) (y : M) :
          f (x + y) = f x + f y

          The proposition that the function preserves addition

          structure AddMonoidHom (M : Type u_10) (N : Type u_11) [AddZeroClass M] [AddZeroClass N] extends ZeroHom :
          Type (max u_10 u_11)

          M →+ N is the type of functions M → N that preserve the AddZeroClass structure.

          AddMonoidHom is also used for group homomorphisms.

          When possible, instead of parametrizing results over (f : M →+ N), you should parametrize over (F : Type*) [AddMonoidHomClass F M N] (f : F).

          When you extend this structure, make sure to extend AddMonoidHomClass.

          • toFun : MN
          • map_zero' : (self).toFun 0 = 0
          • map_add' : ∀ (x y : M), (self).toFun (x + y) = (self).toFun x + (self).toFun y

            The proposition that the function preserves addition

          Instances For

            M →+ N denotes the type of additive monoid homomorphisms from M to N.

            Equations
            Instances For
              class AddMonoidHomClass (F : Type u_10) (M : Type u_11) (N : Type u_12) [AddZeroClass M] [AddZeroClass N] [FunLike F M N] extends AddHomClass , ZeroHomClass :

              AddMonoidHomClass F M N states that F is a type of AddZeroClass-preserving homomorphisms.

              You should also extend this typeclass when you extend AddMonoidHom.

                Instances
                  structure OneHom (M : Type u_10) (N : Type u_11) [One M] [One N] :
                  Type (max u_10 u_11)

                  OneHom M N is the type of functions M → N that preserve one.

                  When possible, instead of parametrizing results over (f : OneHom M N), you should parametrize over (F : Type*) [OneHomClass F M N] (f : F).

                  When you extend this structure, make sure to also extend OneHomClass.

                  • toFun : MN

                    The underlying function

                  • map_one' : self.toFun 1 = 1

                    The proposition that the function preserves 1

                  Instances For
                    theorem OneHom.map_one' {M : Type u_10} {N : Type u_11} [One M] [One N] (self : OneHom M N) :
                    self.toFun 1 = 1

                    The proposition that the function preserves 1

                    class OneHomClass (F : Type u_10) (M : outParam (Type u_11)) (N : outParam (Type u_12)) [One M] [One N] [FunLike F M N] :

                    OneHomClass F M N states that F is a type of one-preserving homomorphisms. You should extend this typeclass when you extend OneHom.

                    • map_one : ∀ (f : F), f 1 = 1

                      The proposition that the function preserves 1

                    Instances
                      theorem OneHomClass.map_one {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [One M] [One N] [FunLike F M N] [self : OneHomClass F M N] (f : F) :
                      f 1 = 1

                      The proposition that the function preserves 1

                      instance ZeroHom.funLike {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] :
                      FunLike (ZeroHom M N) M N
                      Equations
                      • ZeroHom.funLike = { coe := ZeroHom.toFun, coe_injective' := }
                      theorem ZeroHom.funLike.proof_1 {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : ZeroHom M N) (g : ZeroHom M N) (h : f.toFun = g.toFun) :
                      f = g
                      instance OneHom.funLike {M : Type u_4} {N : Type u_5} [One M] [One N] :
                      FunLike (OneHom M N) M N
                      Equations
                      • OneHom.funLike = { coe := OneHom.toFun, coe_injective' := }
                      instance ZeroHom.zeroHomClass {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] :
                      Equations
                      • =
                      instance OneHom.oneHomClass {M : Type u_4} {N : Type u_5} [One M] [One N] :
                      Equations
                      • =
                      @[simp]
                      theorem map_zero {M : Type u_4} {N : Type u_5} {F : Type u_9} [Zero M] [Zero N] [FunLike F M N] [ZeroHomClass F M N] (f : F) :
                      f 0 = 0
                      @[simp]
                      theorem map_one {M : Type u_4} {N : Type u_5} {F : Type u_9} [One M] [One N] [FunLike F M N] [OneHomClass F M N] (f : F) :
                      f 1 = 1
                      theorem map_comp_zero {ι : Type u_1} {M : Type u_4} {N : Type u_5} {F : Type u_9} [Zero M] [Zero N] [FunLike F M N] [ZeroHomClass F M N] (f : F) :
                      f 0 = 0
                      theorem map_comp_one {ι : Type u_1} {M : Type u_4} {N : Type u_5} {F : Type u_9} [One M] [One N] [FunLike F M N] [OneHomClass F M N] (f : F) :
                      f 1 = 1
                      theorem Subsingleton.of_zeroHomClass {M : Type u_4} {N : Type u_5} {F : Type u_9} [Zero M] [Zero N] [FunLike F M N] [Subsingleton M] [ZeroHomClass F M N] :
                      theorem Subsingleton.of_oneHomClass {M : Type u_4} {N : Type u_5} {F : Type u_9} [One M] [One N] [FunLike F M N] [Subsingleton M] [OneHomClass F M N] :

                      In principle this could be an instance, but in practice it causes performance issues.

                      instance instSubsingletonZeroHom {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [Subsingleton M] :
                      Equations
                      • =
                      instance instSubsingletonOneHom {M : Type u_4} {N : Type u_5} [One M] [One N] [Subsingleton M] :
                      Equations
                      • =
                      theorem map_eq_zero_iff {M : Type u_4} {N : Type u_5} {F : Type u_9} [Zero M] [Zero N] [FunLike F M N] [ZeroHomClass F M N] (f : F) (hf : Function.Injective f) {x : M} :
                      f x = 0 x = 0
                      theorem map_eq_one_iff {M : Type u_4} {N : Type u_5} {F : Type u_9} [One M] [One N] [FunLike F M N] [OneHomClass F M N] (f : F) (hf : Function.Injective f) {x : M} :
                      f x = 1 x = 1
                      theorem map_ne_zero_iff {R : Type u_10} {S : Type u_11} {F : Type u_12} [Zero R] [Zero S] [FunLike F R S] [ZeroHomClass F R S] (f : F) (hf : Function.Injective f) {x : R} :
                      f x 0 x 0
                      theorem map_ne_one_iff {R : Type u_10} {S : Type u_11} {F : Type u_12} [One R] [One S] [FunLike F R S] [OneHomClass F R S] (f : F) (hf : Function.Injective f) {x : R} :
                      f x 1 x 1
                      theorem ne_zero_of_map {R : Type u_10} {S : Type u_11} {F : Type u_12} [Zero R] [Zero S] [FunLike F R S] [ZeroHomClass F R S] {f : F} {x : R} (hx : f x 0) :
                      x 0
                      theorem ne_one_of_map {R : Type u_10} {S : Type u_11} {F : Type u_12} [One R] [One S] [FunLike F R S] [OneHomClass F R S] {f : F} {x : R} (hx : f x 1) :
                      x 1
                      def ZeroHomClass.toZeroHom {M : Type u_4} {N : Type u_5} {F : Type u_9} [Zero M] [Zero N] [FunLike F M N] [ZeroHomClass F M N] (f : F) :

                      Turn an element of a type F satisfying ZeroHomClass F M N into an actual ZeroHom. This is declared as the default coercion from F to ZeroHom M N.

                      Equations
                      • f = { toFun := f, map_zero' := }
                      Instances For
                        def OneHomClass.toOneHom {M : Type u_4} {N : Type u_5} {F : Type u_9} [One M] [One N] [FunLike F M N] [OneHomClass F M N] (f : F) :
                        OneHom M N

                        Turn an element of a type F satisfying OneHomClass F M N into an actual OneHom. This is declared as the default coercion from F to OneHom M N.

                        Equations
                        • f = { toFun := f, map_one' := }
                        Instances For
                          instance instCoeTCZeroHomOfZeroHomClass {M : Type u_4} {N : Type u_5} {F : Type u_9} [Zero M] [Zero N] [FunLike F M N] [ZeroHomClass F M N] :
                          CoeTC F (ZeroHom M N)

                          Any type satisfying ZeroHomClass can be cast into ZeroHom via ZeroHomClass.toZeroHom.

                          Equations
                          • instCoeTCZeroHomOfZeroHomClass = { coe := ZeroHomClass.toZeroHom }
                          instance instCoeTCOneHomOfOneHomClass {M : Type u_4} {N : Type u_5} {F : Type u_9} [One M] [One N] [FunLike F M N] [OneHomClass F M N] :
                          CoeTC F (OneHom M N)

                          Any type satisfying OneHomClass can be cast into OneHom via OneHomClass.toOneHom.

                          Equations
                          • instCoeTCOneHomOfOneHomClass = { coe := OneHomClass.toOneHom }
                          @[simp]
                          theorem ZeroHom.coe_coe {M : Type u_4} {N : Type u_5} {F : Type u_9} [Zero M] [Zero N] [FunLike F M N] [ZeroHomClass F M N] (f : F) :
                          f = f
                          @[simp]
                          theorem OneHom.coe_coe {M : Type u_4} {N : Type u_5} {F : Type u_9} [One M] [One N] [FunLike F M N] [OneHomClass F M N] (f : F) :
                          f = f
                          structure MulHom (M : Type u_10) (N : Type u_11) [Mul M] [Mul N] :
                          Type (max u_10 u_11)

                          M →ₙ* N is the type of functions M → N that preserve multiplication. The in the notation stands for "non-unital" because it is intended to match the notation for NonUnitalAlgHom and NonUnitalRingHom, so a MulHom is a non-unital monoid hom.

                          When possible, instead of parametrizing results over (f : M →ₙ* N), you should parametrize over (F : Type*) [MulHomClass F M N] (f : F). When you extend this structure, make sure to extend MulHomClass.

                          • toFun : MN

                            The underlying function

                          • map_mul' : ∀ (x y : M), self.toFun (x * y) = self.toFun x * self.toFun y

                            The proposition that the function preserves multiplication

                          Instances For
                            theorem MulHom.map_mul' {M : Type u_10} {N : Type u_11} [Mul M] [Mul N] (self : M →ₙ* N) (x : M) (y : M) :
                            self.toFun (x * y) = self.toFun x * self.toFun y

                            The proposition that the function preserves multiplication

                            M →ₙ* N denotes the type of multiplication-preserving maps from M to N.

                            Equations
                            Instances For
                              class MulHomClass (F : Type u_10) (M : outParam (Type u_11)) (N : outParam (Type u_12)) [Mul M] [Mul N] [FunLike F M N] :

                              MulHomClass F M N states that F is a type of multiplication-preserving homomorphisms.

                              You should declare an instance of this typeclass when you extend MulHom.

                              • map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y

                                The proposition that the function preserves multiplication

                              Instances
                                theorem MulHomClass.map_mul {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [Mul M] [Mul N] [FunLike F M N] [self : MulHomClass F M N] (f : F) (x : M) (y : M) :
                                f (x * y) = f x * f y

                                The proposition that the function preserves multiplication

                                instance AddHom.funLike {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
                                FunLike (AddHom M N) M N
                                Equations
                                • AddHom.funLike = { coe := AddHom.toFun, coe_injective' := }
                                theorem AddHom.funLike.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (g : AddHom M N) (h : f.toFun = g.toFun) :
                                f = g
                                instance MulHom.funLike {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
                                FunLike (M →ₙ* N) M N
                                Equations
                                • MulHom.funLike = { coe := MulHom.toFun, coe_injective' := }
                                instance AddHom.addHomClass {M : Type u_4} {N : Type u_5} [Add M] [Add N] :

                                AddHom is a type of addition-preserving homomorphisms

                                Equations
                                • =
                                instance MulHom.mulHomClass {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :

                                MulHom is a type of multiplication-preserving homomorphisms

                                Equations
                                • =
                                @[simp]
                                theorem map_add {M : Type u_4} {N : Type u_5} {F : Type u_9} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (x : M) (y : M) :
                                f (x + y) = f x + f y
                                @[simp]
                                theorem map_mul {M : Type u_4} {N : Type u_5} {F : Type u_9} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (x : M) (y : M) :
                                f (x * y) = f x * f y
                                @[simp]
                                theorem map_comp_add {ι : Type u_1} {M : Type u_4} {N : Type u_5} {F : Type u_9} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (g : ιM) (h : ιM) :
                                f (g + h) = f g + f h
                                @[simp]
                                theorem map_comp_mul {ι : Type u_1} {M : Type u_4} {N : Type u_5} {F : Type u_9} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (g : ιM) (h : ιM) :
                                f (g * h) = f g * f h
                                def AddHomClass.toAddHom {M : Type u_4} {N : Type u_5} {F : Type u_9} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) :
                                AddHom M N

                                Turn an element of a type F satisfying AddHomClass F M N into an actual AddHom. This is declared as the default coercion from F to M →ₙ+ N.

                                Equations
                                • f = { toFun := f, map_add' := }
                                Instances For
                                  def MulHomClass.toMulHom {M : Type u_4} {N : Type u_5} {F : Type u_9} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) :

                                  Turn an element of a type F satisfying MulHomClass F M N into an actual MulHom. This is declared as the default coercion from F to M →ₙ* N.

                                  Equations
                                  • f = { toFun := f, map_mul' := }
                                  Instances For
                                    instance instCoeTCAddHomOfAddHomClass {M : Type u_4} {N : Type u_5} {F : Type u_9} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] :
                                    CoeTC F (AddHom M N)

                                    Any type satisfying AddHomClass can be cast into AddHom via AddHomClass.toAddHom.

                                    Equations
                                    • instCoeTCAddHomOfAddHomClass = { coe := AddHomClass.toAddHom }
                                    instance instCoeTCMulHomOfMulHomClass {M : Type u_4} {N : Type u_5} {F : Type u_9} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] :
                                    CoeTC F (M →ₙ* N)

                                    Any type satisfying MulHomClass can be cast into MulHom via MulHomClass.toMulHom.

                                    Equations
                                    • instCoeTCMulHomOfMulHomClass = { coe := MulHomClass.toMulHom }
                                    @[simp]
                                    theorem AddHom.coe_coe {M : Type u_4} {N : Type u_5} {F : Type u_9} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) :
                                    f = f
                                    @[simp]
                                    theorem MulHom.coe_coe {M : Type u_4} {N : Type u_5} {F : Type u_9} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) :
                                    f = f
                                    structure MonoidHom (M : Type u_10) (N : Type u_11) [MulOneClass M] [MulOneClass N] extends OneHom :
                                    Type (max u_10 u_11)

                                    M →* N is the type of functions M → N that preserve the Monoid structure. MonoidHom is also used for group homomorphisms.

                                    When possible, instead of parametrizing results over (f : M →+ N), you should parametrize over (F : Type*) [MonoidHomClass F M N] (f : F).

                                    When you extend this structure, make sure to extend MonoidHomClass.

                                    • toFun : MN
                                    • map_one' : (self).toFun 1 = 1
                                    • map_mul' : ∀ (x y : M), (self).toFun (x * y) = (self).toFun x * (self).toFun y

                                      The proposition that the function preserves multiplication

                                    Instances For

                                      M →* N denotes the type of monoid homomorphisms from M to N.

                                      Equations
                                      Instances For
                                        class MonoidHomClass (F : Type u_10) (M : outParam (Type u_11)) (N : outParam (Type u_12)) [MulOneClass M] [MulOneClass N] [FunLike F M N] extends MulHomClass , OneHomClass :

                                        MonoidHomClass F M N states that F is a type of Monoid-preserving homomorphisms. You should also extend this typeclass when you extend MonoidHom.

                                          Instances
                                            theorem AddMonoidHom.instFunLike.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : M →+ N) (h : (fun (f : M →+ N) => (f).toFun) f = (fun (f : M →+ N) => (f).toFun) g) :
                                            f = g
                                            instance AddMonoidHom.instFunLike {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] :
                                            FunLike (M →+ N) M N
                                            Equations
                                            • AddMonoidHom.instFunLike = { coe := fun (f : M →+ N) => (f).toFun, coe_injective' := }
                                            instance MonoidHom.instFunLike {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] :
                                            FunLike (M →* N) M N
                                            Equations
                                            • MonoidHom.instFunLike = { coe := fun (f : M →* N) => (f).toFun, coe_injective' := }
                                            Equations
                                            • =
                                            instance MonoidHom.instMonoidHomClass {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] :
                                            Equations
                                            • =
                                            Equations
                                            • =
                                            Equations
                                            • =
                                            theorem AddMonoidHomClass.toAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} {F : Type u_3} [AddZeroClass M] [AddZeroClass N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) :
                                            (f).toFun 0 = 0
                                            def AddMonoidHomClass.toAddMonoidHom {M : Type u_4} {N : Type u_5} {F : Type u_9} [AddZeroClass M] [AddZeroClass N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) :
                                            M →+ N

                                            Turn an element of a type F satisfying AddMonoidHomClass F M N into an actual MonoidHom. This is declared as the default coercion from F to M →+ N.

                                            Equations
                                            • f = let __src := f; let __src_1 := f; { toFun := __src.toFun, map_zero' := , map_add' := }
                                            Instances For
                                              theorem AddMonoidHomClass.toAddMonoidHom.proof_2 {M : Type u_2} {N : Type u_1} {F : Type u_3} [AddZeroClass M] [AddZeroClass N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (x : M) (y : M) :
                                              (f).toFun (x + y) = (f).toFun x + (f).toFun y
                                              def MonoidHomClass.toMonoidHom {M : Type u_4} {N : Type u_5} {F : Type u_9} [MulOneClass M] [MulOneClass N] [FunLike F M N] [MonoidHomClass F M N] (f : F) :
                                              M →* N

                                              Turn an element of a type F satisfying MonoidHomClass F M N into an actual MonoidHom. This is declared as the default coercion from F to M →* N.

                                              Equations
                                              • f = let __src := f; let __src_1 := f; { toFun := __src.toFun, map_one' := , map_mul' := }
                                              Instances For
                                                instance instCoeTCAddMonoidHomOfAddMonoidHomClass {M : Type u_4} {N : Type u_5} {F : Type u_9} [AddZeroClass M] [AddZeroClass N] [FunLike F M N] [AddMonoidHomClass F M N] :
                                                CoeTC F (M →+ N)

                                                Any type satisfying AddMonoidHomClass can be cast into AddMonoidHom via AddMonoidHomClass.toAddMonoidHom.

                                                Equations
                                                • instCoeTCAddMonoidHomOfAddMonoidHomClass = { coe := AddMonoidHomClass.toAddMonoidHom }
                                                instance instCoeTCMonoidHomOfMonoidHomClass {M : Type u_4} {N : Type u_5} {F : Type u_9} [MulOneClass M] [MulOneClass N] [FunLike F M N] [MonoidHomClass F M N] :
                                                CoeTC F (M →* N)

                                                Any type satisfying MonoidHomClass can be cast into MonoidHom via MonoidHomClass.toMonoidHom.

                                                Equations
                                                • instCoeTCMonoidHomOfMonoidHomClass = { coe := MonoidHomClass.toMonoidHom }
                                                @[simp]
                                                theorem AddMonoidHom.coe_coe {M : Type u_4} {N : Type u_5} {F : Type u_9} [AddZeroClass M] [AddZeroClass N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) :
                                                f = f
                                                @[simp]
                                                theorem MonoidHom.coe_coe {M : Type u_4} {N : Type u_5} {F : Type u_9} [MulOneClass M] [MulOneClass N] [FunLike F M N] [MonoidHomClass F M N] (f : F) :
                                                f = f
                                                theorem map_add_eq_zero {M : Type u_4} {N : Type u_5} {F : Type u_9} [AddZeroClass M] [AddZeroClass N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) {a : M} {b : M} (h : a + b = 0) :
                                                f a + f b = 0
                                                theorem map_mul_eq_one {M : Type u_4} {N : Type u_5} {F : Type u_9} [MulOneClass M] [MulOneClass N] [FunLike F M N] [MonoidHomClass F M N] (f : F) {a : M} {b : M} (h : a * b = 1) :
                                                f a * f b = 1
                                                theorem map_sub' {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [SubNegMonoid G] [SubNegMonoid H] [AddMonoidHomClass F G H] (f : F) (hf : ∀ (a : G), f (-a) = -f a) (a : G) (b : G) :
                                                f (a - b) = f a - f b
                                                theorem map_div' {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F) (hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹) (a : G) (b : G) :
                                                f (a / b) = f a / f b
                                                theorem map_comp_sub' {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [SubNegMonoid G] [SubNegMonoid H] [AddMonoidHomClass F G H] (f : F) (hf : ∀ (a : G), f (-a) = -f a) (g : ιG) (h : ιG) :
                                                f (g - h) = f g - f h
                                                theorem map_comp_div' {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F) (hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹) (g : ιG) (h : ιG) :
                                                f (g / h) = f g / f h
                                                @[simp]
                                                theorem map_neg {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (a : G) :
                                                f (-a) = -f a

                                                Additive group homomorphisms preserve negation.

                                                @[simp]
                                                theorem map_inv {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (a : G) :
                                                f a⁻¹ = (f a)⁻¹

                                                Group homomorphisms preserve inverse.

                                                @[simp]
                                                theorem map_comp_neg {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (g : ιG) :
                                                f (-g) = -f g
                                                @[simp]
                                                theorem map_comp_inv {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ιG) :
                                                f g⁻¹ = (f g)⁻¹
                                                theorem map_add_neg {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (a : G) (b : G) :
                                                f (a + -b) = f a + -f b

                                                Additive group homomorphisms preserve subtraction.

                                                theorem map_mul_inv {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (a : G) (b : G) :
                                                f (a * b⁻¹) = f a * (f b)⁻¹

                                                Group homomorphisms preserve division.

                                                theorem map_comp_add_neg {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (g : ιG) (h : ιG) :
                                                f (g + -h) = f g + -f h
                                                theorem map_comp_mul_inv {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ιG) (h : ιG) :
                                                f (g * h⁻¹) = f g * (f h)⁻¹
                                                @[simp]
                                                theorem map_sub {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (a : G) (b : G) :
                                                f (a - b) = f a - f b

                                                Additive group homomorphisms preserve subtraction.

                                                @[simp]
                                                theorem map_div {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (a : G) (b : G) :
                                                f (a / b) = f a / f b

                                                Group homomorphisms preserve division.

                                                @[simp]
                                                theorem map_comp_sub {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (g : ιG) (h : ιG) :
                                                f (g - h) = f g - f h
                                                @[simp]
                                                theorem map_comp_div {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ιG) (h : ιG) :
                                                f (g / h) = f g / f h
                                                abbrev map_nsmul.match_1 (motive : Prop) :
                                                ∀ (x : ), (Unitmotive 0)(∀ (n : ), motive n.succ)motive x
                                                Equations
                                                • =
                                                Instances For
                                                  @[simp]
                                                  theorem map_nsmul {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [AddMonoid G] [AddMonoid H] [AddMonoidHomClass F G H] (f : F) (n : ) (a : G) :
                                                  f (n a) = n f a
                                                  @[simp]
                                                  theorem map_pow {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (a : G) (n : ) :
                                                  f (a ^ n) = f a ^ n
                                                  @[simp]
                                                  theorem map_comp_nsmul {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (g : ιG) (n : ) :
                                                  f (n g) = n f g
                                                  @[simp]
                                                  theorem map_comp_pow {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ιG) (n : ) :
                                                  f (g ^ n) = f g ^ n
                                                  abbrev map_zsmul'.match_1 (motive : Prop) :
                                                  ∀ (x : ), (∀ (n : ), motive (Int.ofNat n))(∀ (n : ), motive (Int.negSucc n))motive x
                                                  Equations
                                                  • =
                                                  Instances For
                                                    theorem map_zsmul' {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [SubNegMonoid G] [SubNegMonoid H] [AddMonoidHomClass F G H] (f : F) (hf : ∀ (x : G), f (-x) = -f x) (a : G) (n : ) :
                                                    f (n a) = n f a
                                                    theorem map_zpow' {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F) (hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹) (a : G) (n : ) :
                                                    f (a ^ n) = f a ^ n
                                                    @[simp]
                                                    theorem map_comp_zsmul' {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [SubNegMonoid G] [SubNegMonoid H] [AddMonoidHomClass F G H] (f : F) (hf : ∀ (x : G), f (-x) = -f x) (g : ιG) (n : ) :
                                                    f (n g) = n f g
                                                    @[simp]
                                                    theorem map_comp_zpow' {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F) (hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹) (g : ιG) (n : ) :
                                                    f (g ^ n) = f g ^ n
                                                    @[simp]
                                                    theorem map_zsmul {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (n : ) (g : G) :
                                                    f (n g) = n f g

                                                    Additive group homomorphisms preserve integer scaling.

                                                    @[simp]
                                                    theorem map_zpow {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : G) (n : ) :
                                                    f (g ^ n) = f g ^ n

                                                    Group homomorphisms preserve integer power.

                                                    theorem map_comp_zsmul {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [AddGroup G] [SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (g : ιG) (n : ) :
                                                    f (n g) = n f g
                                                    theorem map_comp_zpow {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [FunLike F G H] [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ιG) (n : ) :
                                                    f (g ^ n) = f g ^ n

                                                    Bundled morphisms can be down-cast to weaker bundlings

                                                    instance AddMonoidHom.coeToZeroHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] :
                                                    Coe (M →+ N) (ZeroHom M N)

                                                    AddMonoidHom down-cast to a ZeroHom, forgetting the additive property

                                                    Equations
                                                    • AddMonoidHom.coeToZeroHom = { coe := AddMonoidHom.toZeroHom }
                                                    instance MonoidHom.coeToOneHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] :
                                                    Coe (M →* N) (OneHom M N)

                                                    MonoidHom down-cast to a OneHom, forgetting the multiplicative property.

                                                    Equations
                                                    • MonoidHom.coeToOneHom = { coe := MonoidHom.toOneHom }
                                                    instance AddMonoidHom.coeToAddHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] :
                                                    Coe (M →+ N) (AddHom M N)

                                                    AddMonoidHom down-cast to an AddHom, forgetting the 0-preserving property.

                                                    Equations
                                                    • AddMonoidHom.coeToAddHom = { coe := AddMonoidHom.toAddHom }
                                                    instance MonoidHom.coeToMulHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] :
                                                    Coe (M →* N) (M →ₙ* N)

                                                    MonoidHom down-cast to a MulHom, forgetting the 1-preserving property.

                                                    Equations
                                                    • MonoidHom.coeToMulHom = { coe := MonoidHom.toMulHom }
                                                    @[simp]
                                                    theorem ZeroHom.coe_mk {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (f : MN) (h1 : f 0 = 0) :
                                                    { toFun := f, map_zero' := h1 } = f
                                                    @[simp]
                                                    theorem OneHom.coe_mk {M : Type u_4} {N : Type u_5} [One M] [One N] (f : MN) (h1 : f 1 = 1) :
                                                    { toFun := f, map_one' := h1 } = f
                                                    @[simp]
                                                    theorem ZeroHom.toFun_eq_coe {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (f : ZeroHom M N) :
                                                    f.toFun = f
                                                    @[simp]
                                                    theorem OneHom.toFun_eq_coe {M : Type u_4} {N : Type u_5} [One M] [One N] (f : OneHom M N) :
                                                    f.toFun = f
                                                    @[simp]
                                                    theorem AddHom.coe_mk {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : MN) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
                                                    { toFun := f, map_add' := hmul } = f
                                                    @[simp]
                                                    theorem MulHom.coe_mk {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : MN) (hmul : ∀ (x y : M), f (x * y) = f x * f y) :
                                                    { toFun := f, map_mul' := hmul } = f
                                                    @[simp]
                                                    theorem AddHom.toFun_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : AddHom M N) :
                                                    f.toFun = f
                                                    @[simp]
                                                    theorem MulHom.toFun_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) :
                                                    f.toFun = f
                                                    @[simp]
                                                    theorem AddMonoidHom.coe_mk {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : ZeroHom M N) (hmul : ∀ (x y : M), f.toFun (x + y) = f.toFun x + f.toFun y) :
                                                    { toZeroHom := f, map_add' := hmul } = f
                                                    @[simp]
                                                    theorem MonoidHom.coe_mk {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : OneHom M N) (hmul : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y) :
                                                    { toOneHom := f, map_mul' := hmul } = f
                                                    @[simp]
                                                    theorem AddMonoidHom.toZeroHom_coe {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                                    f = f
                                                    @[simp]
                                                    theorem MonoidHom.toOneHom_coe {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                                    f = f
                                                    @[simp]
                                                    theorem AddMonoidHom.toAddHom_coe {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                                    (f).toFun = f
                                                    @[simp]
                                                    theorem MonoidHom.toMulHom_coe {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                                    (f).toFun = f
                                                    theorem AddMonoidHom.toFun_eq_coe {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                                    (f).toFun = f
                                                    theorem MonoidHom.toFun_eq_coe {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                                    (f).toFun = f
                                                    theorem ZeroHom.ext {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] ⦃f : ZeroHom M N ⦃g : ZeroHom M N (h : ∀ (x : M), f x = g x) :
                                                    f = g
                                                    theorem OneHom.ext {M : Type u_4} {N : Type u_5} [One M] [One N] ⦃f : OneHom M N ⦃g : OneHom M N (h : ∀ (x : M), f x = g x) :
                                                    f = g
                                                    theorem AddHom.ext {M : Type u_4} {N : Type u_5} [Add M] [Add N] ⦃f : AddHom M N ⦃g : AddHom M N (h : ∀ (x : M), f x = g x) :
                                                    f = g
                                                    theorem MulHom.ext {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] ⦃f : M →ₙ* N ⦃g : M →ₙ* N (h : ∀ (x : M), f x = g x) :
                                                    f = g
                                                    theorem AddMonoidHom.ext {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] ⦃f : M →+ N ⦃g : M →+ N (h : ∀ (x : M), f x = g x) :
                                                    f = g
                                                    theorem MonoidHom.ext {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] ⦃f : M →* N ⦃g : M →* N (h : ∀ (x : M), f x = g x) :
                                                    f = g
                                                    def AddMonoidHom.mk' {M : Type u_4} {G : Type u_7} [AddGroup G] [AddZeroClass M] (f : MG) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :
                                                    M →+ G

                                                    Makes an additive group homomorphism from a proof that the map preserves addition.

                                                    Equations
                                                    Instances For
                                                      theorem AddMonoidHom.mk'.proof_1 {M : Type u_2} {G : Type u_1} [AddGroup G] [AddZeroClass M] (f : MG) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :
                                                      f 0 = 0
                                                      @[simp]
                                                      theorem AddMonoidHom.mk'_apply {M : Type u_4} {G : Type u_7} [AddGroup G] [AddZeroClass M] (f : MG) (map_mul : ∀ (a b : M), f (a + b) = f a + f b) :
                                                      (AddMonoidHom.mk' f map_mul) = f
                                                      @[simp]
                                                      theorem MonoidHom.mk'_apply {M : Type u_4} {G : Type u_7} [Group G] [MulOneClass M] (f : MG) (map_mul : ∀ (a b : M), f (a * b) = f a * f b) :
                                                      (MonoidHom.mk' f map_mul) = f
                                                      def MonoidHom.mk' {M : Type u_4} {G : Type u_7} [Group G] [MulOneClass M] (f : MG) (map_mul : ∀ (a b : M), f (a * b) = f a * f b) :
                                                      M →* G

                                                      Makes a group homomorphism from a proof that the map preserves multiplication.

                                                      Equations
                                                      • MonoidHom.mk' f map_mul = { toFun := f, map_one' := , map_mul' := map_mul }
                                                      Instances For
                                                        @[simp]
                                                        theorem ZeroHom.mk_coe {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (f : ZeroHom M N) (h1 : f 0 = 0) :
                                                        { toFun := f, map_zero' := h1 } = f
                                                        @[simp]
                                                        theorem OneHom.mk_coe {M : Type u_4} {N : Type u_5} [One M] [One N] (f : OneHom M N) (h1 : f 1 = 1) :
                                                        { toFun := f, map_one' := h1 } = f
                                                        @[simp]
                                                        theorem AddHom.mk_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : AddHom M N) (hmul : ∀ (x y : M), f (x + y) = f x + f y) :
                                                        { toFun := f, map_add' := hmul } = f
                                                        @[simp]
                                                        theorem MulHom.mk_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (hmul : ∀ (x y : M), f (x * y) = f x * f y) :
                                                        { toFun := f, map_mul' := hmul } = f
                                                        @[simp]
                                                        theorem AddMonoidHom.mk_coe {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hmul : ∀ (x y : M), (f).toFun (x + y) = (f).toFun x + (f).toFun y) :
                                                        { toZeroHom := f, map_add' := hmul } = f
                                                        @[simp]
                                                        theorem MonoidHom.mk_coe {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (hmul : ∀ (x y : M), (f).toFun (x * y) = (f).toFun x * (f).toFun y) :
                                                        { toOneHom := f, map_mul' := hmul } = f
                                                        def ZeroHom.copy {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (f : ZeroHom M N) (f' : MN) (h : f' = f) :

                                                        Copy of a ZeroHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                                                        Equations
                                                        • f.copy f' h = { toFun := f', map_zero' := }
                                                        Instances For
                                                          theorem ZeroHom.copy.proof_1 {M : Type u_2} {N : Type u_1} [Zero M] [Zero N] (f : ZeroHom M N) (f' : MN) (h : f' = f) :
                                                          f' 0 = 0
                                                          def OneHom.copy {M : Type u_4} {N : Type u_5} [One M] [One N] (f : OneHom M N) (f' : MN) (h : f' = f) :
                                                          OneHom M N

                                                          Copy of a OneHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                                                          Equations
                                                          • f.copy f' h = { toFun := f', map_one' := }
                                                          Instances For
                                                            @[simp]
                                                            theorem ZeroHom.coe_copy {M : Type u_4} {N : Type u_5} :
                                                            ∀ {x : Zero M} {x_1 : Zero N} (f : ZeroHom M N) (f' : MN) (h : f' = f), (f.copy f' h) = f'
                                                            @[simp]
                                                            theorem OneHom.coe_copy {M : Type u_4} {N : Type u_5} :
                                                            ∀ {x : One M} {x_1 : One N} (f : OneHom M N) (f' : MN) (h : f' = f), (f.copy f' h) = f'
                                                            theorem ZeroHom.coe_copy_eq {M : Type u_4} {N : Type u_5} :
                                                            ∀ {x : Zero M} {x_1 : Zero N} (f : ZeroHom M N) (f' : MN) (h : f' = f), f.copy f' h = f
                                                            theorem OneHom.coe_copy_eq {M : Type u_4} {N : Type u_5} :
                                                            ∀ {x : One M} {x_1 : One N} (f : OneHom M N) (f' : MN) (h : f' = f), f.copy f' h = f
                                                            theorem AddHom.copy.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (f' : MN) (h : f' = f) (x : M) (y : M) :
                                                            f' (x + y) = f' x + f' y
                                                            def AddHom.copy {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : AddHom M N) (f' : MN) (h : f' = f) :
                                                            AddHom M N

                                                            Copy of an AddHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                                                            Equations
                                                            • f.copy f' h = { toFun := f', map_add' := }
                                                            Instances For
                                                              def MulHom.copy {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (f' : MN) (h : f' = f) :

                                                              Copy of a MulHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                                                              Equations
                                                              • f.copy f' h = { toFun := f', map_mul' := }
                                                              Instances For
                                                                @[simp]
                                                                theorem AddHom.coe_copy {M : Type u_4} {N : Type u_5} :
                                                                ∀ {x : Add M} {x_1 : Add N} (f : AddHom M N) (f' : MN) (h : f' = f), (f.copy f' h) = f'
                                                                @[simp]
                                                                theorem MulHom.coe_copy {M : Type u_4} {N : Type u_5} :
                                                                ∀ {x : Mul M} {x_1 : Mul N} (f : M →ₙ* N) (f' : MN) (h : f' = f), (f.copy f' h) = f'
                                                                theorem AddHom.coe_copy_eq {M : Type u_4} {N : Type u_5} :
                                                                ∀ {x : Add M} {x_1 : Add N} (f : AddHom M N) (f' : MN) (h : f' = f), f.copy f' h = f
                                                                theorem MulHom.coe_copy_eq {M : Type u_4} {N : Type u_5} :
                                                                ∀ {x : Mul M} {x_1 : Mul N} (f : M →ₙ* N) (f' : MN) (h : f' = f), f.copy f' h = f
                                                                def AddMonoidHom.copy {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (f' : MN) (h : f' = f) :
                                                                M →+ N

                                                                Copy of an AddMonoidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                                                                Equations
                                                                • f.copy f' h = let __src := (f).copy f' h; let __src_1 := (f).copy f' h; { toZeroHom := __src, map_add' := }
                                                                Instances For
                                                                  theorem AddMonoidHom.copy.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (f' : MN) (h : f' = f) (x : M) (y : M) :
                                                                  ((f).copy f' h).toFun (x + y) = ((f).copy f' h).toFun x + ((f).copy f' h).toFun y
                                                                  def MonoidHom.copy {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (f' : MN) (h : f' = f) :
                                                                  M →* N

                                                                  Copy of a MonoidHom with a new toFun equal to the old one. Useful to fix definitional equalities.

                                                                  Equations
                                                                  • f.copy f' h = let __src := (f).copy f' h; let __src_1 := (f).copy f' h; { toOneHom := __src, map_mul' := }
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem AddMonoidHom.coe_copy {M : Type u_4} {N : Type u_5} :
                                                                    ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} (f : M →+ N) (f' : MN) (h : f' = f), (f.copy f' h) = f'
                                                                    @[simp]
                                                                    theorem MonoidHom.coe_copy {M : Type u_4} {N : Type u_5} :
                                                                    ∀ {x : MulOneClass M} {x_1 : MulOneClass N} (f : M →* N) (f' : MN) (h : f' = f), (f.copy f' h) = f'
                                                                    theorem AddMonoidHom.copy_eq {M : Type u_4} {N : Type u_5} :
                                                                    ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} (f : M →+ N) (f' : MN) (h : f' = f), f.copy f' h = f
                                                                    theorem MonoidHom.copy_eq {M : Type u_4} {N : Type u_5} :
                                                                    ∀ {x : MulOneClass M} {x_1 : MulOneClass N} (f : M →* N) (f' : MN) (h : f' = f), f.copy f' h = f
                                                                    theorem ZeroHom.map_zero {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (f : ZeroHom M N) :
                                                                    f 0 = 0
                                                                    theorem OneHom.map_one {M : Type u_4} {N : Type u_5} [One M] [One N] (f : OneHom M N) :
                                                                    f 1 = 1
                                                                    theorem AddMonoidHom.map_zero {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                                                    f 0 = 0

                                                                    If f is an additive monoid homomorphism then f 0 = 0.

                                                                    theorem MonoidHom.map_one {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                                                    f 1 = 1

                                                                    If f is a monoid homomorphism then f 1 = 1.

                                                                    theorem AddHom.map_add {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : AddHom M N) (a : M) (b : M) :
                                                                    f (a + b) = f a + f b
                                                                    theorem MulHom.map_mul {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (a : M) (b : M) :
                                                                    f (a * b) = f a * f b
                                                                    theorem AddMonoidHom.map_add {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (a : M) (b : M) :
                                                                    f (a + b) = f a + f b

                                                                    If f is an additive monoid homomorphism then f (a + b) = f a + f b.

                                                                    theorem MonoidHom.map_mul {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (a : M) (b : M) :
                                                                    f (a * b) = f a * f b

                                                                    If f is a monoid homomorphism then f (a * b) = f a * f b.

                                                                    abbrev AddMonoidHom.map_exists_right_neg.match_1 {M : Type u_1} [AddZeroClass M] {x : M} (motive : (∃ (y : M), x + y = 0)Prop) :
                                                                    ∀ (hx : ∃ (y : M), x + y = 0), (∀ (y : M) (hy : x + y = 0), motive )motive hx
                                                                    Equations
                                                                    • =
                                                                    Instances For
                                                                      theorem AddMonoidHom.map_exists_right_neg {M : Type u_4} {N : Type u_5} {F : Type u_9} [AddZeroClass M] [AddZeroClass N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) {x : M} (hx : ∃ (y : M), x + y = 0) :
                                                                      ∃ (y : N), f x + y = 0

                                                                      Given an AddMonoid homomorphism f : M →+ N and an element x : M, if x has a right inverse, then f x has a right inverse too.

                                                                      theorem MonoidHom.map_exists_right_inv {M : Type u_4} {N : Type u_5} {F : Type u_9} [MulOneClass M] [MulOneClass N] [FunLike F M N] [MonoidHomClass F M N] (f : F) {x : M} (hx : ∃ (y : M), x * y = 1) :
                                                                      ∃ (y : N), f x * y = 1

                                                                      Given a monoid homomorphism f : M →* N and an element x : M, if x has a right inverse, then f x has a right inverse too. For elements invertible on both sides see IsUnit.map.

                                                                      abbrev AddMonoidHom.map_exists_left_neg.match_1 {M : Type u_1} [AddZeroClass M] {x : M} (motive : (∃ (y : M), y + x = 0)Prop) :
                                                                      ∀ (hx : ∃ (y : M), y + x = 0), (∀ (y : M) (hy : y + x = 0), motive )motive hx
                                                                      Equations
                                                                      • =
                                                                      Instances For
                                                                        theorem AddMonoidHom.map_exists_left_neg {M : Type u_4} {N : Type u_5} {F : Type u_9} [AddZeroClass M] [AddZeroClass N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) {x : M} (hx : ∃ (y : M), y + x = 0) :
                                                                        ∃ (y : N), y + f x = 0

                                                                        Given an AddMonoid homomorphism f : M →+ N and an element x : M, if x has a left inverse, then f x has a left inverse too. For elements invertible on both sides see IsAddUnit.map.

                                                                        theorem MonoidHom.map_exists_left_inv {M : Type u_4} {N : Type u_5} {F : Type u_9} [MulOneClass M] [MulOneClass N] [FunLike F M N] [MonoidHomClass F M N] (f : F) {x : M} (hx : ∃ (y : M), y * x = 1) :
                                                                        ∃ (y : N), y * f x = 1

                                                                        Given a monoid homomorphism f : M →* N and an element x : M, if x has a left inverse, then f x has a left inverse too. For elements invertible on both sides see IsUnit.map.

                                                                        theorem ZeroHom.id.proof_1 (M : Type u_1) [Zero M] :
                                                                        (fun (x : M) => x) 0 = (fun (x : M) => x) 0
                                                                        def ZeroHom.id (M : Type u_10) [Zero M] :

                                                                        The identity map from a type with zero to itself.

                                                                        Equations
                                                                        • ZeroHom.id M = { toFun := fun (x : M) => x, map_zero' := }
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem ZeroHom.id_apply (M : Type u_10) [Zero M] (x : M) :
                                                                          (ZeroHom.id M) x = x
                                                                          @[simp]
                                                                          theorem OneHom.id_apply (M : Type u_10) [One M] (x : M) :
                                                                          (OneHom.id M) x = x
                                                                          def OneHom.id (M : Type u_10) [One M] :
                                                                          OneHom M M

                                                                          The identity map from a type with 1 to itself.

                                                                          Equations
                                                                          • OneHom.id M = { toFun := fun (x : M) => x, map_one' := }
                                                                          Instances For
                                                                            theorem AddHom.id.proof_1 (M : Type u_1) [Add M] :
                                                                            ∀ (x x_1 : M), (fun (x : M) => x) (x + x_1) = (fun (x : M) => x) (x + x_1)
                                                                            def AddHom.id (M : Type u_10) [Add M] :
                                                                            AddHom M M

                                                                            The identity map from a type with addition to itself.

                                                                            Equations
                                                                            • AddHom.id M = { toFun := fun (x : M) => x, map_add' := }
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem MulHom.id_apply (M : Type u_10) [Mul M] (x : M) :
                                                                              (MulHom.id M) x = x
                                                                              @[simp]
                                                                              theorem AddHom.id_apply (M : Type u_10) [Add M] (x : M) :
                                                                              (AddHom.id M) x = x
                                                                              def MulHom.id (M : Type u_10) [Mul M] :

                                                                              The identity map from a type with multiplication to itself.

                                                                              Equations
                                                                              • MulHom.id M = { toFun := fun (x : M) => x, map_mul' := }
                                                                              Instances For
                                                                                theorem AddMonoidHom.id.proof_1 (M : Type u_1) [AddZeroClass M] :
                                                                                (fun (x : M) => x) 0 = (fun (x : M) => x) 0
                                                                                def AddMonoidHom.id (M : Type u_10) [AddZeroClass M] :
                                                                                M →+ M

                                                                                The identity map from an additive monoid to itself.

                                                                                Equations
                                                                                • AddMonoidHom.id M = { toFun := fun (x : M) => x, map_zero' := , map_add' := }
                                                                                Instances For
                                                                                  theorem AddMonoidHom.id.proof_2 (M : Type u_1) [AddZeroClass M] :
                                                                                  ∀ (x x_1 : M), { toFun := fun (x : M) => x, map_zero' := }.toFun (x + x_1) = { toFun := fun (x : M) => x, map_zero' := }.toFun (x + x_1)
                                                                                  @[simp]
                                                                                  theorem MonoidHom.id_apply (M : Type u_10) [MulOneClass M] (x : M) :
                                                                                  (MonoidHom.id M) x = x
                                                                                  @[simp]
                                                                                  theorem AddMonoidHom.id_apply (M : Type u_10) [AddZeroClass M] (x : M) :
                                                                                  def MonoidHom.id (M : Type u_10) [MulOneClass M] :
                                                                                  M →* M

                                                                                  The identity map from a monoid to itself.

                                                                                  Equations
                                                                                  • MonoidHom.id M = { toFun := fun (x : M) => x, map_one' := , map_mul' := }
                                                                                  Instances For
                                                                                    def ZeroHom.comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [Zero M] [Zero N] [Zero P] (hnp : ZeroHom N P) (hmn : ZeroHom M N) :

                                                                                    Composition of ZeroHoms as a ZeroHom.

                                                                                    Equations
                                                                                    • hnp.comp hmn = { toFun := hnp hmn, map_zero' := }
                                                                                    Instances For
                                                                                      theorem ZeroHom.comp.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [Zero M] [Zero N] [Zero P] (hnp : ZeroHom N P) (hmn : ZeroHom M N) :
                                                                                      hnp (hmn 0) = 0
                                                                                      def OneHom.comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [One M] [One N] [One P] (hnp : OneHom N P) (hmn : OneHom M N) :
                                                                                      OneHom M P

                                                                                      Composition of OneHoms as a OneHom.

                                                                                      Equations
                                                                                      • hnp.comp hmn = { toFun := hnp hmn, map_one' := }
                                                                                      Instances For
                                                                                        def AddHom.comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (hnp : AddHom N P) (hmn : AddHom M N) :
                                                                                        AddHom M P

                                                                                        Composition of AddHoms as an AddHom.

                                                                                        Equations
                                                                                        • hnp.comp hmn = { toFun := hnp hmn, map_add' := }
                                                                                        Instances For
                                                                                          theorem AddHom.comp.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [Add M] [Add N] [Add P] (hnp : AddHom N P) (hmn : AddHom M N) (x : M) (y : M) :
                                                                                          hnp (hmn (x + y)) = hnp (hmn x) + hnp (hmn y)
                                                                                          def MulHom.comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (hnp : N →ₙ* P) (hmn : M →ₙ* N) :

                                                                                          Composition of MulHoms as a MulHom.

                                                                                          Equations
                                                                                          • hnp.comp hmn = { toFun := hnp hmn, map_mul' := }
                                                                                          Instances For
                                                                                            theorem AddMonoidHom.comp.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (hnp : N →+ P) (hmn : M →+ N) :
                                                                                            hnp (hmn 0) = 0
                                                                                            def AddMonoidHom.comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (hnp : N →+ P) (hmn : M →+ N) :
                                                                                            M →+ P

                                                                                            Composition of additive monoid morphisms as an additive monoid morphism.

                                                                                            Equations
                                                                                            • hnp.comp hmn = { toFun := hnp hmn, map_zero' := , map_add' := }
                                                                                            Instances For
                                                                                              theorem AddMonoidHom.comp.proof_2 {M : Type u_3} {N : Type u_2} {P : Type u_1} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (hnp : N →+ P) (hmn : M →+ N) (a : M) (a : M) :
                                                                                              hnp (hmn (a✝ + a)) = hnp (hmn a✝) + hnp (hmn a)
                                                                                              def MonoidHom.comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (hnp : N →* P) (hmn : M →* N) :
                                                                                              M →* P

                                                                                              Composition of monoid morphisms as a monoid morphism.

                                                                                              Equations
                                                                                              • hnp.comp hmn = { toFun := hnp hmn, map_one' := , map_mul' := }
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem ZeroHom.coe_comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [Zero M] [Zero N] [Zero P] (g : ZeroHom N P) (f : ZeroHom M N) :
                                                                                                (g.comp f) = g f
                                                                                                @[simp]
                                                                                                theorem OneHom.coe_comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) :
                                                                                                (g.comp f) = g f
                                                                                                @[simp]
                                                                                                theorem AddHom.coe_comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (g : AddHom N P) (f : AddHom M N) :
                                                                                                (g.comp f) = g f
                                                                                                @[simp]
                                                                                                theorem MulHom.coe_comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) :
                                                                                                (g.comp f) = g f
                                                                                                @[simp]
                                                                                                theorem AddMonoidHom.coe_comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (g : N →+ P) (f : M →+ N) :
                                                                                                (g.comp f) = g f
                                                                                                @[simp]
                                                                                                theorem MonoidHom.coe_comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (g : N →* P) (f : M →* N) :
                                                                                                (g.comp f) = g f
                                                                                                theorem ZeroHom.comp_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Zero M] [Zero N] [Zero P] (g : ZeroHom N P) (f : ZeroHom M N) (x : M) :
                                                                                                (g.comp f) x = g (f x)
                                                                                                theorem OneHom.comp_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [One M] [One N] [One P] (g : OneHom N P) (f : OneHom M N) (x : M) :
                                                                                                (g.comp f) x = g (f x)
                                                                                                theorem AddHom.comp_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (g : AddHom N P) (f : AddHom M N) (x : M) :
                                                                                                (g.comp f) x = g (f x)
                                                                                                theorem MulHom.comp_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (g : N →ₙ* P) (f : M →ₙ* N) (x : M) :
                                                                                                (g.comp f) x = g (f x)
                                                                                                theorem AddMonoidHom.comp_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (g : N →+ P) (f : M →+ N) (x : M) :
                                                                                                (g.comp f) x = g (f x)
                                                                                                theorem MonoidHom.comp_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (g : N →* P) (f : M →* N) (x : M) :
                                                                                                (g.comp f) x = g (f x)
                                                                                                theorem ZeroHom.comp_assoc {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [Zero M] [Zero N] [Zero P] [Zero Q] (f : ZeroHom M N) (g : ZeroHom N P) (h : ZeroHom P Q) :
                                                                                                (h.comp g).comp f = h.comp (g.comp f)

                                                                                                Composition of additive monoid homomorphisms is associative.

                                                                                                theorem OneHom.comp_assoc {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [One M] [One N] [One P] [One Q] (f : OneHom M N) (g : OneHom N P) (h : OneHom P Q) :
                                                                                                (h.comp g).comp f = h.comp (g.comp f)

                                                                                                Composition of monoid homomorphisms is associative.

                                                                                                theorem AddHom.comp_assoc {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [Add M] [Add N] [Add P] [Add Q] (f : AddHom M N) (g : AddHom N P) (h : AddHom P Q) :
                                                                                                (h.comp g).comp f = h.comp (g.comp f)
                                                                                                theorem MulHom.comp_assoc {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [Mul M] [Mul N] [Mul P] [Mul Q] (f : M →ₙ* N) (g : N →ₙ* P) (h : P →ₙ* Q) :
                                                                                                (h.comp g).comp f = h.comp (g.comp f)
                                                                                                theorem AddMonoidHom.comp_assoc {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] [AddZeroClass Q] (f : M →+ N) (g : N →+ P) (h : P →+ Q) :
                                                                                                (h.comp g).comp f = h.comp (g.comp f)
                                                                                                theorem MonoidHom.comp_assoc {M : Type u_4} {N : Type u_5} {P : Type u_6} {Q : Type u_10} [MulOneClass M] [MulOneClass N] [MulOneClass P] [MulOneClass Q] (f : M →* N) (g : N →* P) (h : P →* Q) :
                                                                                                (h.comp g).comp f = h.comp (g.comp f)
                                                                                                theorem ZeroHom.cancel_right {M : Type u_4} {N : Type u_5} {P : Type u_6} [Zero M] [Zero N] [Zero P] {g₁ : ZeroHom N P} {g₂ : ZeroHom N P} {f : ZeroHom M N} (hf : Function.Surjective f) :
                                                                                                g₁.comp f = g₂.comp f g₁ = g₂
                                                                                                theorem OneHom.cancel_right {M : Type u_4} {N : Type u_5} {P : Type u_6} [One M] [One N] [One P] {g₁ : OneHom N P} {g₂ : OneHom N P} {f : OneHom M N} (hf : Function.Surjective f) :
                                                                                                g₁.comp f = g₂.comp f g₁ = g₂
                                                                                                theorem AddHom.cancel_right {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] {g₁ : AddHom N P} {g₂ : AddHom N P} {f : AddHom M N} (hf : Function.Surjective f) :
                                                                                                g₁.comp f = g₂.comp f g₁ = g₂
                                                                                                theorem MulHom.cancel_right {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] {g₁ : N →ₙ* P} {g₂ : N →ₙ* P} {f : M →ₙ* N} (hf : Function.Surjective f) :
                                                                                                g₁.comp f = g₂.comp f g₁ = g₂
                                                                                                theorem AddMonoidHom.cancel_right {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] {g₁ : N →+ P} {g₂ : N →+ P} {f : M →+ N} (hf : Function.Surjective f) :
                                                                                                g₁.comp f = g₂.comp f g₁ = g₂
                                                                                                theorem MonoidHom.cancel_right {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] {g₁ : N →* P} {g₂ : N →* P} {f : M →* N} (hf : Function.Surjective f) :
                                                                                                g₁.comp f = g₂.comp f g₁ = g₂
                                                                                                theorem ZeroHom.cancel_left {M : Type u_4} {N : Type u_5} {P : Type u_6} [Zero M] [Zero N] [Zero P] {g : ZeroHom N P} {f₁ : ZeroHom M N} {f₂ : ZeroHom M N} (hg : Function.Injective g) :
                                                                                                g.comp f₁ = g.comp f₂ f₁ = f₂
                                                                                                theorem OneHom.cancel_left {M : Type u_4} {N : Type u_5} {P : Type u_6} [One M] [One N] [One P] {g : OneHom N P} {f₁ : OneHom M N} {f₂ : OneHom M N} (hg : Function.Injective g) :
                                                                                                g.comp f₁ = g.comp f₂ f₁ = f₂
                                                                                                theorem AddHom.cancel_left {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] {g : AddHom N P} {f₁ : AddHom M N} {f₂ : AddHom M N} (hg : Function.Injective g) :
                                                                                                g.comp f₁ = g.comp f₂ f₁ = f₂
                                                                                                theorem MulHom.cancel_left {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] {g : N →ₙ* P} {f₁ : M →ₙ* N} {f₂ : M →ₙ* N} (hg : Function.Injective g) :
                                                                                                g.comp f₁ = g.comp f₂ f₁ = f₂
                                                                                                theorem AddMonoidHom.cancel_left {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] {g : N →+ P} {f₁ : M →+ N} {f₂ : M →+ N} (hg : Function.Injective g) :
                                                                                                g.comp f₁ = g.comp f₂ f₁ = f₂
                                                                                                theorem MonoidHom.cancel_left {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] {g : N →* P} {f₁ : M →* N} {f₂ : M →* N} (hg : Function.Injective g) :
                                                                                                g.comp f₁ = g.comp f₂ f₁ = f₂
                                                                                                theorem AddMonoidHom.toZeroHom_injective {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] :
                                                                                                Function.Injective AddMonoidHom.toZeroHom
                                                                                                theorem MonoidHom.toOneHom_injective {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] :
                                                                                                Function.Injective MonoidHom.toOneHom
                                                                                                theorem AddMonoidHom.toAddHom_injective {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] :
                                                                                                Function.Injective AddMonoidHom.toAddHom
                                                                                                theorem MonoidHom.toMulHom_injective {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] :
                                                                                                Function.Injective MonoidHom.toMulHom
                                                                                                @[simp]
                                                                                                theorem ZeroHom.comp_id {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (f : ZeroHom M N) :
                                                                                                f.comp (ZeroHom.id M) = f
                                                                                                @[simp]
                                                                                                theorem OneHom.comp_id {M : Type u_4} {N : Type u_5} [One M] [One N] (f : OneHom M N) :
                                                                                                f.comp (OneHom.id M) = f
                                                                                                @[simp]
                                                                                                theorem AddHom.comp_id {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : AddHom M N) :
                                                                                                f.comp (AddHom.id M) = f
                                                                                                @[simp]
                                                                                                theorem MulHom.comp_id {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) :
                                                                                                f.comp (MulHom.id M) = f
                                                                                                @[simp]
                                                                                                theorem AddMonoidHom.comp_id {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                                                                                f.comp (AddMonoidHom.id M) = f
                                                                                                @[simp]
                                                                                                theorem MonoidHom.comp_id {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                                                                                f.comp (MonoidHom.id M) = f
                                                                                                @[simp]
                                                                                                theorem ZeroHom.id_comp {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (f : ZeroHom M N) :
                                                                                                (ZeroHom.id N).comp f = f
                                                                                                @[simp]
                                                                                                theorem OneHom.id_comp {M : Type u_4} {N : Type u_5} [One M] [One N] (f : OneHom M N) :
                                                                                                (OneHom.id N).comp f = f
                                                                                                @[simp]
                                                                                                theorem AddHom.id_comp {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : AddHom M N) :
                                                                                                (AddHom.id N).comp f = f
                                                                                                @[simp]
                                                                                                theorem MulHom.id_comp {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) :
                                                                                                (MulHom.id N).comp f = f
                                                                                                @[simp]
                                                                                                theorem AddMonoidHom.id_comp {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
                                                                                                (AddMonoidHom.id N).comp f = f
                                                                                                @[simp]
                                                                                                theorem MonoidHom.id_comp {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) :
                                                                                                (MonoidHom.id N).comp f = f
                                                                                                theorem AddMonoidHom.map_nsmul {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (a : M) (n : ) :
                                                                                                f (n a) = n f a
                                                                                                theorem MonoidHom.map_pow {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* N) (a : M) (n : ) :
                                                                                                f (a ^ n) = f a ^ n
                                                                                                theorem AddMonoidHom.map_zsmul' {M : Type u_4} {N : Type u_5} [SubNegMonoid M] [SubNegMonoid N] (f : M →+ N) (hf : ∀ (x : M), f (-x) = -f x) (a : M) (n : ) :
                                                                                                f (n a) = n f a
                                                                                                theorem MonoidHom.map_zpow' {M : Type u_4} {N : Type u_5} [DivInvMonoid M] [DivInvMonoid N] (f : M →* N) (hf : ∀ (x : M), f x⁻¹ = (f x)⁻¹) (a : M) (n : ) :
                                                                                                f (a ^ n) = f a ^ n
                                                                                                def Monoid.End (M : Type u_4) [MulOneClass M] :
                                                                                                Type u_4

                                                                                                The monoid of endomorphisms.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  instance Monoid.End.instFunLike (M : Type u_4) [MulOneClass M] :
                                                                                                  Equations
                                                                                                  Equations
                                                                                                  • =
                                                                                                  instance Monoid.End.instOne (M : Type u_4) [MulOneClass M] :
                                                                                                  Equations
                                                                                                  instance Monoid.End.instMul (M : Type u_4) [MulOneClass M] :
                                                                                                  Equations
                                                                                                  instance Monoid.End.inst (M : Type u_4) [MulOneClass M] :
                                                                                                  Equations
                                                                                                  Equations
                                                                                                  @[simp]
                                                                                                  theorem Monoid.End.coe_pow (M : Type u_4) [MulOneClass M] (f : Monoid.End M) (n : ) :
                                                                                                  (f ^ n) = (f)^[n]
                                                                                                  @[simp]
                                                                                                  theorem Monoid.coe_one (M : Type u_4) [MulOneClass M] :
                                                                                                  1 = id
                                                                                                  @[simp]
                                                                                                  theorem Monoid.coe_mul (M : Type u_4) [MulOneClass M] (f : Monoid.End M) (g : Monoid.End M) :
                                                                                                  (f * g) = f g
                                                                                                  def AddMonoid.End (A : Type u_10) [AddZeroClass A] :
                                                                                                  Type u_10

                                                                                                  The monoid of endomorphisms.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    Equations
                                                                                                    Equations
                                                                                                    @[simp]
                                                                                                    theorem AddMonoid.End.coe_one (A : Type u_10) [AddZeroClass A] :
                                                                                                    1 = id
                                                                                                    @[simp]
                                                                                                    theorem AddMonoid.End.coe_mul (A : Type u_10) [AddZeroClass A] (f : AddMonoid.End A) (g : AddMonoid.End A) :
                                                                                                    (f * g) = f g
                                                                                                    Equations
                                                                                                    @[simp]
                                                                                                    theorem AddMonoid.End.coe_pow (A : Type u_10) [AddZeroClass A] (f : AddMonoid.End A) (n : ) :
                                                                                                    (f ^ n) = (f)^[n]
                                                                                                    theorem instZeroZeroHom.proof_1 {M : Type u_2} {N : Type u_1} [Zero M] [Zero N] :
                                                                                                    (fun (x : M) => 0) 0 = (fun (x : M) => 0) 0
                                                                                                    instance instZeroZeroHom {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] :

                                                                                                    0 is the homomorphism sending all elements to 0.

                                                                                                    Equations
                                                                                                    • instZeroZeroHom = { zero := { toFun := fun (x : M) => 0, map_zero' := } }
                                                                                                    instance instOneOneHom {M : Type u_4} {N : Type u_5} [One M] [One N] :
                                                                                                    One (OneHom M N)

                                                                                                    1 is the homomorphism sending all elements to 1.

                                                                                                    Equations
                                                                                                    • instOneOneHom = { one := { toFun := fun (x : M) => 1, map_one' := } }
                                                                                                    theorem instZeroAddHom.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass N] :
                                                                                                    MM0 = 0 + 0
                                                                                                    instance instZeroAddHom {M : Type u_4} {N : Type u_5} [Add M] [AddZeroClass N] :
                                                                                                    Zero (AddHom M N)

                                                                                                    0 is the additive homomorphism sending all elements to 0

                                                                                                    Equations
                                                                                                    • instZeroAddHom = { zero := { toFun := fun (x : M) => 0, map_add' := } }
                                                                                                    instance instOneMulHom {M : Type u_4} {N : Type u_5} [Mul M] [MulOneClass N] :
                                                                                                    One (M →ₙ* N)

                                                                                                    1 is the multiplicative homomorphism sending all elements to 1.

                                                                                                    Equations
                                                                                                    • instOneMulHom = { one := { toFun := fun (x : M) => 1, map_mul' := } }
                                                                                                    theorem instZeroAddMonoidHom.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass N] :
                                                                                                    MM0 = 0 + 0
                                                                                                    instance instZeroAddMonoidHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] :
                                                                                                    Zero (M →+ N)

                                                                                                    0 is the additive monoid homomorphism sending all elements to 0.

                                                                                                    Equations
                                                                                                    • instZeroAddMonoidHom = { zero := { toFun := fun (x : M) => 0, map_zero' := , map_add' := } }
                                                                                                    theorem instZeroAddMonoidHom.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] :
                                                                                                    (fun (x : M) => 0) 0 = (fun (x : M) => 0) 0
                                                                                                    instance instOneMonoidHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] :
                                                                                                    One (M →* N)

                                                                                                    1 is the monoid homomorphism sending all elements to 1.

                                                                                                    Equations
                                                                                                    • instOneMonoidHom = { one := { toFun := fun (x : M) => 1, map_one' := , map_mul' := } }
                                                                                                    @[simp]
                                                                                                    theorem ZeroHom.zero_apply {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] (x : M) :
                                                                                                    0 x = 0
                                                                                                    @[simp]
                                                                                                    theorem OneHom.one_apply {M : Type u_4} {N : Type u_5} [One M] [One N] (x : M) :
                                                                                                    1 x = 1
                                                                                                    @[simp]
                                                                                                    theorem AddMonoidHom.zero_apply {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (x : M) :
                                                                                                    0 x = 0
                                                                                                    @[simp]
                                                                                                    theorem MonoidHom.one_apply {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (x : M) :
                                                                                                    1 x = 1
                                                                                                    @[simp]
                                                                                                    theorem ZeroHom.zero_comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [Zero M] [Zero N] [Zero P] (f : ZeroHom M N) :
                                                                                                    @[simp]
                                                                                                    theorem OneHom.one_comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [One M] [One N] [One P] (f : OneHom M N) :
                                                                                                    @[simp]
                                                                                                    theorem ZeroHom.comp_zero {M : Type u_4} {N : Type u_5} {P : Type u_6} [Zero M] [Zero N] [Zero P] (f : ZeroHom N P) :
                                                                                                    f.comp 0 = 0
                                                                                                    @[simp]
                                                                                                    theorem OneHom.comp_one {M : Type u_4} {N : Type u_5} {P : Type u_6} [One M] [One N] [One P] (f : OneHom N P) :
                                                                                                    f.comp 1 = 1
                                                                                                    instance instInhabitedZeroHom {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] :
                                                                                                    Equations
                                                                                                    • instInhabitedZeroHom = { default := 0 }
                                                                                                    instance instInhabitedOneHom {M : Type u_4} {N : Type u_5} [One M] [One N] :
                                                                                                    Equations
                                                                                                    • instInhabitedOneHom = { default := 1 }
                                                                                                    instance instInhabitedAddHom {M : Type u_4} {N : Type u_5} [Add M] [AddZeroClass N] :
                                                                                                    Equations
                                                                                                    • instInhabitedAddHom = { default := 0 }
                                                                                                    instance instInhabitedMulHom {M : Type u_4} {N : Type u_5} [Mul M] [MulOneClass N] :
                                                                                                    Equations
                                                                                                    • instInhabitedMulHom = { default := 1 }
                                                                                                    instance instInhabitedAddMonoidHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] :
                                                                                                    Equations
                                                                                                    • instInhabitedAddMonoidHom = { default := 0 }
                                                                                                    instance instInhabitedMonoidHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] :
                                                                                                    Equations
                                                                                                    • instInhabitedMonoidHom = { default := 1 }
                                                                                                    @[simp]
                                                                                                    theorem AddMonoidHom.zero_comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) :
                                                                                                    @[simp]
                                                                                                    theorem MonoidHom.one_comp {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) :
                                                                                                    @[simp]
                                                                                                    theorem AddMonoidHom.comp_zero {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : N →+ P) :
                                                                                                    f.comp 0 = 0
                                                                                                    @[simp]
                                                                                                    theorem MonoidHom.comp_one {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : N →* P) :
                                                                                                    f.comp 1 = 1
                                                                                                    theorem AddMonoidHom.map_neg {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] (f : α →+ β) (a : α) :
                                                                                                    f (-a) = -f a

                                                                                                    Additive group homomorphisms preserve negation.

                                                                                                    theorem MonoidHom.map_inv {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] (f : α →* β) (a : α) :
                                                                                                    f a⁻¹ = (f a)⁻¹

                                                                                                    Group homomorphisms preserve inverse.

                                                                                                    theorem AddMonoidHom.map_zsmul {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] (f : α →+ β) (g : α) (n : ) :
                                                                                                    f (n g) = n f g

                                                                                                    Additive group homomorphisms preserve integer scaling.

                                                                                                    theorem MonoidHom.map_zpow {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] (f : α →* β) (g : α) (n : ) :
                                                                                                    f (g ^ n) = f g ^ n

                                                                                                    Group homomorphisms preserve integer power.

                                                                                                    theorem AddMonoidHom.map_sub {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] (f : α →+ β) (g : α) (h : α) :
                                                                                                    f (g - h) = f g - f h

                                                                                                    Additive group homomorphisms preserve subtraction.

                                                                                                    theorem MonoidHom.map_div {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] (f : α →* β) (g : α) (h : α) :
                                                                                                    f (g / h) = f g / f h

                                                                                                    Group homomorphisms preserve division.

                                                                                                    theorem AddMonoidHom.map_add_neg {α : Type u_2} {β : Type u_3} [AddGroup α] [SubtractionMonoid β] (f : α →+ β) (g : α) (h : α) :
                                                                                                    f (g + -h) = f g + -f h

                                                                                                    Additive group homomorphisms preserve subtraction.

                                                                                                    theorem MonoidHom.map_mul_inv {α : Type u_2} {β : Type u_3} [Group α] [DivisionMonoid β] (f : α →* β) (g : α) (h : α) :
                                                                                                    f (g * h⁻¹) = f g * (f h)⁻¹

                                                                                                    Group homomorphisms preserve division.