Documentation

Mathlib.Algebra.Group.Hom.Instances

Instances on spaces of monoid and group morphisms #

We endow the space of monoid morphisms M →* N with a CommMonoid structure when the target is commutative, through pointwise multiplication, and with a CommGroup structure when the target is a commutative group. We also prove the same instances for additive situations.

Since these structures permit morphisms of morphisms, we also provide some composition-like operations.

Finally, we provide the Ring structure on AddMonoid.End.

theorem AddMonoidHom.addCommMonoid.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddCommMonoid N] :
∀ (a : M →+ N), a + 0 = a
theorem AddMonoidHom.addCommMonoid.proof_4 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] (n : ) (f : M →+ N) :
n f 0 = 0
theorem AddMonoidHom.addCommMonoid.proof_6 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddCommMonoid N] (f : M →+ N) :
(fun (n : ) (f : M →+ N) => { toFun := fun (x : M) => n f x, map_zero' := , map_add' := }) 0 f = 0

(M →+ N) is an AddCommMonoid if N is commutative.

Equations
theorem AddMonoidHom.addCommMonoid.proof_5 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddCommMonoid N] (n : ) (f : M →+ N) (x : M) (y : M) :
n f (x + y) = n f x + n f y
theorem AddMonoidHom.addCommMonoid.proof_7 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddCommMonoid N] (n : ) (f : M →+ N) :
(fun (n : ) (f : M →+ N) => { toFun := fun (x : M) => n f x, map_zero' := , map_add' := }) (n + 1) f = (fun (n : ) (f : M →+ N) => { toFun := fun (x : M) => n f x, map_zero' := , map_add' := }) n f + f
theorem AddMonoidHom.addCommMonoid.proof_8 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddCommMonoid N] :
∀ (a b : M →+ N), a + b = b + a
theorem AddMonoidHom.addCommMonoid.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddCommMonoid N] :
∀ (a b c : M →+ N), a + b + c = a + (b + c)
theorem AddMonoidHom.addCommMonoid.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddCommMonoid N] :
∀ (a : M →+ N), 0 + a = a
instance MonoidHom.commMonoid {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] :

(M →* N) is a CommMonoid if N is commutative.

Equations
theorem AddMonoidHom.addCommGroup.proof_3 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] (n : ) (f : M →+ G) (x : M) (y : M) :
n f (x + y) = n f x + n f y
instance AddMonoidHom.addCommGroup {M : Type u_1} {G : Type u_2} [AddZeroClass M] [AddCommGroup G] :

If G is an additive commutative group, then M →+ G is an additive commutative group too.

Equations
  • AddMonoidHom.addCommGroup = let __src := AddMonoidHom.addCommMonoid; AddCommGroup.mk
theorem AddMonoidHom.addCommGroup.proof_4 {M : Type u_1} {G : Type u_2} [AddZeroClass M] [AddCommGroup G] (f : M →+ G) :
(fun (n : ) (f : M →+ G) => { toFun := fun (x : M) => n f x, map_zero' := , map_add' := }) 0 f = 0
theorem AddMonoidHom.addCommGroup.proof_7 {M : Type u_1} {G : Type u_2} [AddZeroClass M] [AddCommGroup G] :
∀ (a : M →+ G), -a + a = 0
theorem AddMonoidHom.addCommGroup.proof_8 {M : Type u_1} {G : Type u_2} [AddZeroClass M] [AddCommGroup G] (a : M →+ G) (b : M →+ G) :
a + b = b + a
theorem AddMonoidHom.addCommGroup.proof_2 {M : Type u_2} {G : Type u_1} [AddZeroClass M] [AddCommGroup G] (n : ) (f : M →+ G) :
n f 0 = 0
theorem AddMonoidHom.addCommGroup.proof_5 {M : Type u_1} {G : Type u_2} [AddZeroClass M] [AddCommGroup G] (n : ) (f : M →+ G) :
(fun (n : ) (f : M →+ G) => { toFun := fun (x : M) => n f x, map_zero' := , map_add' := }) (Int.ofNat n.succ) f = (fun (n : ) (f : M →+ G) => { toFun := fun (x : M) => n f x, map_zero' := , map_add' := }) (Int.ofNat n) f + f
theorem AddMonoidHom.addCommGroup.proof_1 {M : Type u_1} {G : Type u_2} [AddZeroClass M] [AddCommGroup G] :
∀ (a b : M →+ G), a - b = a + -b
theorem AddMonoidHom.addCommGroup.proof_6 {M : Type u_1} {G : Type u_2} [AddZeroClass M] [AddCommGroup G] (n : ) (f : M →+ G) :
(fun (n : ) (f : M →+ G) => { toFun := fun (x : M) => n f x, map_zero' := , map_add' := }) (Int.negSucc n) f = -(fun (n : ) (f : M →+ G) => { toFun := fun (x : M) => n f x, map_zero' := , map_add' := }) (n.succ) f
instance MonoidHom.commGroup {M : Type u_1} {G : Type u_2} [MulOneClass M] [CommGroup G] :

If G is a commutative group, then M →* G is a commutative group too.

Equations
  • MonoidHom.commGroup = let __src := MonoidHom.commMonoid; CommGroup.mk
Equations
  • AddMonoid.End.instAddCommMonoid = AddMonoidHom.addCommMonoid
@[simp]
theorem AddMonoid.End.zero_apply {M : Type uM} [AddCommMonoid M] (m : M) :
0 m = 0
theorem AddMonoid.End.one_apply {M : Type uM} [AddCommMonoid M] (m : M) :
1 m = m
Equations
  • AddMonoid.End.instAddCommGroup = AddMonoidHom.addCommGroup
Equations
  • AddMonoid.End.instIntCast = { intCast := fun (z : ) => z 1 }
@[simp]
theorem AddMonoid.End.intCast_apply {M : Type uM} [AddCommGroup M] (z : ) (m : M) :
z m = z m

See also AddMonoid.End.intCast_def.

@[deprecated AddMonoid.End.intCast_apply]
theorem AddMonoid.End.int_cast_apply {M : Type uM} [AddCommGroup M] (z : ) (m : M) :
z m = z m

Alias of AddMonoid.End.intCast_apply.


See also AddMonoid.End.intCast_def.

@[simp]
theorem AddMonoidHom.nsmul_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddCommMonoid N] (f : M →+ N) (n : ) (x : M) :
(n f) x = n f x
@[simp]
theorem MonoidHom.pow_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [CommMonoid N] (f : M →* N) (n : ) (x : M) :
(f ^ n) x = f x ^ n

Morphisms of morphisms #

The structures above permit morphisms that themselves produce morphisms, provided the codomain is commutative.

theorem AddMonoidHom.ext_iff₂ {M : Type uM} {N : Type uN} {P : Type uP} :
∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} {f g : M →+ N →+ P}, f = g ∀ (x_3 : M) (y : N), (f x_3) y = (g x_3) y
theorem MonoidHom.ext_iff₂ {M : Type uM} {N : Type uN} {P : Type uP} :
∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} {f g : M →* N →* P}, f = g ∀ (x_3 : M) (y : N), (f x_3) y = (g x_3) y
theorem AddMonoidHom.flip.proof_4 {M : Type u_1} {N : Type u_3} {P : Type u_2} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P} (f : M →+ N →+ P) (y₁ : N) (y₂ : N) :
{ toFun := fun (y : N) => { toFun := fun (x : M) => (f x) y, map_zero' := , map_add' := }, map_zero' := }.toFun (y₁ + y₂) = { toFun := fun (y : N) => { toFun := fun (x : M) => (f x) y, map_zero' := , map_add' := }, map_zero' := }.toFun y₁ + { toFun := fun (y : N) => { toFun := fun (x : M) => (f x) y, map_zero' := , map_add' := }, map_zero' := }.toFun y₂
theorem AddMonoidHom.flip.proof_2 {M : Type u_3} {N : Type u_2} {P : Type u_1} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P} (f : M →+ N →+ P) (y : N) (x₁ : M) (x₂ : M) :
(f (x₁ + x₂)) y = (f x₁) y + (f x₂) y
theorem AddMonoidHom.flip.proof_3 {M : Type u_1} {N : Type u_3} {P : Type u_2} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P} (f : M →+ N →+ P) :
(fun (y : N) => { toFun := fun (x : M) => (f x) y, map_zero' := , map_add' := }) 0 = 0
def AddMonoidHom.flip {M : Type uM} {N : Type uN} {P : Type uP} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P} (f : M →+ N →+ P) :
N →+ M →+ P

flip arguments of f : M →+ N →+ P

Equations
  • f.flip = { toFun := fun (y : N) => { toFun := fun (x : M) => (f x) y, map_zero' := , map_add' := }, map_zero' := , map_add' := }
Instances For
    theorem AddMonoidHom.flip.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} {mM : AddZeroClass M} {mN : AddZeroClass N} {mP : AddCommMonoid P} (f : M →+ N →+ P) (y : N) :
    (f 0) y = 0
    def MonoidHom.flip {M : Type uM} {N : Type uN} {P : Type uP} {mM : MulOneClass M} {mN : MulOneClass N} {mP : CommMonoid P} (f : M →* N →* P) :
    N →* M →* P

    flip arguments of f : M →* N →* P

    Equations
    • f.flip = { toFun := fun (y : N) => { toFun := fun (x : M) => (f x) y, map_one' := , map_mul' := }, map_one' := , map_mul' := }
    Instances For
      @[simp]
      theorem AddMonoidHom.flip_apply {M : Type uM} {N : Type uN} {P : Type uP} :
      ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P) (x_3 : M) (y : N), (f.flip y) x_3 = (f x_3) y
      @[simp]
      theorem MonoidHom.flip_apply {M : Type uM} {N : Type uN} {P : Type uP} :
      ∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P) (x_3 : M) (y : N), (f.flip y) x_3 = (f x_3) y
      theorem AddMonoidHom.map_one₂ {M : Type uM} {N : Type uN} {P : Type uP} :
      ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P) (n : N), (f 0) n = 0
      theorem MonoidHom.map_one₂ {M : Type uM} {N : Type uN} {P : Type uP} :
      ∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P) (n : N), (f 1) n = 1
      theorem AddMonoidHom.map_mul₂ {M : Type uM} {N : Type uN} {P : Type uP} :
      ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P) (m₁ m₂ : M) (n : N), (f (m₁ + m₂)) n = (f m₁) n + (f m₂) n
      theorem MonoidHom.map_mul₂ {M : Type uM} {N : Type uN} {P : Type uP} :
      ∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P) (m₁ m₂ : M) (n : N), (f (m₁ * m₂)) n = (f m₁) n * (f m₂) n
      theorem AddMonoidHom.map_inv₂ {M : Type uM} {N : Type uN} {P : Type uP} :
      ∀ {x : AddGroup M} {x_1 : AddZeroClass N} {x_2 : AddCommGroup P} (f : M →+ N →+ P) (m : M) (n : N), (f (-m)) n = -(f m) n
      theorem MonoidHom.map_inv₂ {M : Type uM} {N : Type uN} {P : Type uP} :
      ∀ {x : Group M} {x_1 : MulOneClass N} {x_2 : CommGroup P} (f : M →* N →* P) (m : M) (n : N), (f m⁻¹) n = ((f m) n)⁻¹
      theorem AddMonoidHom.map_div₂ {M : Type uM} {N : Type uN} {P : Type uP} :
      ∀ {x : AddGroup M} {x_1 : AddZeroClass N} {x_2 : AddCommGroup P} (f : M →+ N →+ P) (m₁ m₂ : M) (n : N), (f (m₁ - m₂)) n = (f m₁) n - (f m₂) n
      theorem MonoidHom.map_div₂ {M : Type uM} {N : Type uN} {P : Type uP} :
      ∀ {x : Group M} {x_1 : MulOneClass N} {x_2 : CommGroup P} (f : M →* N →* P) (m₁ m₂ : M) (n : N), (f (m₁ / m₂)) n = (f m₁) n / (f m₂) n
      def AddMonoidHom.eval {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] :
      M →+ (M →+ N) →+ N

      Evaluation of an AddMonoidHom at a point as an additive monoid homomorphism. See also AddMonoidHom.apply for the evaluation of any function at a point.

      Equations
      Instances For
        @[simp]
        theorem AddMonoidHom.eval_apply_apply {M : Type uM} {N : Type uN} [AddZeroClass M] [AddCommMonoid N] (y : M) (x : M →+ N) :
        (AddMonoidHom.eval y) x = x y
        @[simp]
        theorem MonoidHom.eval_apply_apply {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] (y : M) (x : M →* N) :
        (MonoidHom.eval y) x = x y
        def MonoidHom.eval {M : Type uM} {N : Type uN} [MulOneClass M] [CommMonoid N] :
        M →* (M →* N) →* N

        Evaluation of a MonoidHom at a point as a monoid homomorphism. See also MonoidHom.apply for the evaluation of any function at a point.

        Equations
        Instances For
          def AddMonoidHom.compHom' {M : Type uM} {N : Type uN} {P : Type uP} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ N) :
          (N →+ P) →+ M →+ P

          The expression fun g m ↦ g (f m) as an AddMonoidHom. Equivalently, (fun g ↦ AddMonoidHom.comp g f) as an AddMonoidHom.

          This also exists in a LinearMap version, LinearMap.lcomp.

          Equations
          • f.compHom' = (AddMonoidHom.eval.comp f).flip
          Instances For
            @[simp]
            theorem MonoidHom.compHom'_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* N) (y : N →* P) (x : M) :
            (f.compHom' y) x = y (f x)
            @[simp]
            theorem AddMonoidHom.compHom'_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ N) (y : N →+ P) (x : M) :
            (f.compHom' y) x = y (f x)
            def MonoidHom.compHom' {M : Type uM} {N : Type uN} {P : Type uP} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* N) :
            (N →* P) →* M →* P

            The expression fun g m ↦ g (f m) as a MonoidHom. Equivalently, (fun g ↦ MonoidHom.comp g f) as a MonoidHom.

            Equations
            • f.compHom' = (MonoidHom.eval.comp f).flip
            Instances For
              theorem AddMonoidHom.compHom.proof_2 {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] :
              (fun (g : N →+ P) => { toFun := g.comp, map_zero' := , map_add' := }) 0 = 0
              theorem AddMonoidHom.compHom.proof_1 {M : Type u_1} {N : Type u_3} {P : Type u_2} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P) :
              g.comp 0 = 0
              def AddMonoidHom.compHom {M : Type uM} {N : Type uN} {P : Type uP} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] :
              (N →+ P) →+ (M →+ N) →+ M →+ P

              Composition of additive monoid morphisms (AddMonoidHom.comp) as an additive monoid morphism.

              Note that unlike AddMonoidHom.comp_hom' this requires commutativity of N.

              This also exists in a LinearMap version, LinearMap.llcomp.

              Equations
              • AddMonoidHom.compHom = { toFun := fun (g : N →+ P) => { toFun := g.comp, map_zero' := , map_add' := }, map_zero' := , map_add' := }
              Instances For
                theorem AddMonoidHom.compHom.proof_3 {M : Type u_3} {N : Type u_1} {P : Type u_2} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g₁ : N →+ P) (g₂ : N →+ P) :
                { toFun := fun (g : N →+ P) => { toFun := g.comp, map_zero' := , map_add' := }, map_zero' := }.toFun (g₁ + g₂) = { toFun := fun (g : N →+ P) => { toFun := g.comp, map_zero' := , map_add' := }, map_zero' := }.toFun g₁ + { toFun := fun (g : N →+ P) => { toFun := g.comp, map_zero' := , map_add' := }, map_zero' := }.toFun g₂
                @[simp]
                theorem AddMonoidHom.compHom_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [AddZeroClass M] [AddCommMonoid N] [AddCommMonoid P] (g : N →+ P) (hmn : M →+ N) :
                (AddMonoidHom.compHom g) hmn = g.comp hmn
                @[simp]
                theorem MonoidHom.compHom_apply_apply {M : Type uM} {N : Type uN} {P : Type uP} [MulOneClass M] [CommMonoid N] [CommMonoid P] (g : N →* P) (hmn : M →* N) :
                (MonoidHom.compHom g) hmn = g.comp hmn
                def MonoidHom.compHom {M : Type uM} {N : Type uN} {P : Type uP} [MulOneClass M] [CommMonoid N] [CommMonoid P] :
                (N →* P) →* (M →* N) →* M →* P

                Composition of monoid morphisms (MonoidHom.comp) as a monoid morphism.

                Note that unlike MonoidHom.comp_hom' this requires commutativity of N.

                Equations
                • MonoidHom.compHom = { toFun := fun (g : N →* P) => { toFun := g.comp, map_one' := , map_mul' := }, map_one' := , map_mul' := }
                Instances For
                  def AddMonoidHom.flipHom {M : Type uM} {N : Type uN} {P : Type uP} :
                  {x : AddZeroClass M} → {x_1 : AddZeroClass N} → {x_2 : AddCommMonoid P} → (M →+ N →+ P) →+ N →+ M →+ P

                  Flipping arguments of additive monoid morphisms (AddMonoidHom.flip) as an additive monoid morphism.

                  Equations
                  • AddMonoidHom.flipHom = { toFun := AddMonoidHom.flip, map_zero' := , map_add' := }
                  Instances For
                    theorem AddMonoidHom.flipHom.proof_2 {M : Type u_1} {N : Type u_3} {P : Type u_2} :
                    ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (x_3 x_4 : M →+ N →+ P), { toFun := AddMonoidHom.flip, map_zero' := }.toFun (x_3 + x_4) = { toFun := AddMonoidHom.flip, map_zero' := }.toFun (x_3 + x_4)
                    theorem AddMonoidHom.flipHom.proof_1 {M : Type u_1} {N : Type u_2} {P : Type u_3} :
                    @[simp]
                    theorem MonoidHom.flipHom_apply {M : Type uM} {N : Type uN} {P : Type uP} :
                    ∀ {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P} (f : M →* N →* P), MonoidHom.flipHom f = f.flip
                    @[simp]
                    theorem AddMonoidHom.flipHom_apply {M : Type uM} {N : Type uN} {P : Type uP} :
                    ∀ {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P} (f : M →+ N →+ P), AddMonoidHom.flipHom f = f.flip
                    def MonoidHom.flipHom {M : Type uM} {N : Type uN} {P : Type uP} :
                    {x : MulOneClass M} → {x_1 : MulOneClass N} → {x_2 : CommMonoid P} → (M →* N →* P) →* N →* M →* P

                    Flipping arguments of monoid morphisms (MonoidHom.flip) as a monoid morphism.

                    Equations
                    • MonoidHom.flipHom = { toFun := MonoidHom.flip, map_one' := , map_mul' := }
                    Instances For
                      def AddMonoidHom.compl₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddZeroClass Q] (f : M →+ N →+ P) (g : Q →+ N) :
                      M →+ Q →+ P

                      The expression fun m q ↦ f m (g q) as an AddMonoidHom.

                      Note that the expression fun q n ↦ f (g q) n is simply AddMonoidHom.comp.

                      This also exists as a LinearMap version, LinearMap.compl₂

                      Equations
                      • f.compl₂ g = g.compHom'.comp f
                      Instances For
                        def MonoidHom.compl₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [MulOneClass M] [MulOneClass N] [CommMonoid P] [MulOneClass Q] (f : M →* N →* P) (g : Q →* N) :
                        M →* Q →* P

                        The expression fun m q ↦ f m (g q) as a MonoidHom.

                        Note that the expression fun q n ↦ f (g q) n is simply MonoidHom.comp.

                        Equations
                        • f.compl₂ g = g.compHom'.comp f
                        Instances For
                          @[simp]
                          theorem AddMonoidHom.compl₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddZeroClass Q] (f : M →+ N →+ P) (g : Q →+ N) (m : M) (q : Q) :
                          ((f.compl₂ g) m) q = (f m) (g q)
                          @[simp]
                          theorem MonoidHom.compl₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [MulOneClass M] [MulOneClass N] [CommMonoid P] [MulOneClass Q] (f : M →* N →* P) (g : Q →* N) (m : M) (q : Q) :
                          ((f.compl₂ g) m) q = (f m) (g q)
                          def AddMonoidHom.compr₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M →+ N →+ P) (g : P →+ Q) :
                          M →+ N →+ Q

                          The expression fun m n ↦ g (f m n) as an AddMonoidHom.

                          This also exists as a LinearMap version, LinearMap.compr₂

                          Equations
                          • f.compr₂ g = (AddMonoidHom.compHom g).comp f
                          Instances For
                            def MonoidHom.compr₂ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M →* N →* P) (g : P →* Q) :
                            M →* N →* Q

                            The expression fun m n ↦ g (f m n) as a MonoidHom.

                            Equations
                            • f.compr₂ g = (MonoidHom.compHom g).comp f
                            Instances For
                              @[simp]
                              theorem AddMonoidHom.compr₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] [AddCommMonoid Q] (f : M →+ N →+ P) (g : P →+ Q) (m : M) (n : N) :
                              ((f.compr₂ g) m) n = g ((f m) n)
                              @[simp]
                              theorem MonoidHom.compr₂_apply {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [MulOneClass M] [MulOneClass N] [CommMonoid P] [CommMonoid Q] (f : M →* N →* P) (g : P →* Q) (m : M) (n : N) :
                              ((f.compr₂ g) m) n = g ((f m) n)