Documentation

Mathlib.GroupTheory.GroupAction.Hom

Equivariant homomorphisms #

Main definitions #

The above types have corresponding classes:

Notations #

structure MulActionHom (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] :
Type (max u_2 u_3)

Equivariant functions.

  • toFun : XY

    The underlying function.

  • map_smul' : ∀ (m : M') (x : X), self.toFun (m x) = m self.toFun x

    The proposition that the function preserves the action.

Instances For

Equivariant functions.

Equations
  • One or more equations did not get rendered due to their size.
class SMulHomClass (F : Type u_16) (M : outParam (Type u_17)) (X : outParam (Type u_18)) (Y : outParam (Type u_19)) [SMul M X] [SMul M Y] [FunLike F X Y] :

SMulHomClass F M X Y states that F is a type of morphisms preserving scalar multiplication by M.

You should extend this class when you extend MulActionHom.

  • map_smul : ∀ (f : F) (c : M) (x : X), f (c x) = c f x

    The proposition that the function preserves the action.

Instances
instance instFunLikeMulActionHom (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] :
FunLike (X →[M'] Y) X Y
Equations
instance instSMulHomClassMulActionHomInstFunLikeMulActionHom (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] :
SMulHomClass (X →[M'] Y) M' X Y
Equations
  • =
def SMulHomClass.toMulActionHom {X : Type u_2} {Y : Type u_3} {M : Type u_5} {F : Type u_16} [SMul M X] [SMul M Y] [FunLike F X Y] [SMulHomClass F M X Y] (f : F) :
X →[M] Y

Turn an element of a type F satisfying SMulHomClass F M X Y into an actual MulActionHom. This is declared as the default coercion from F to MulActionHom M X Y.

Equations
  • f = { toFun := f, map_smul' := }
instance MulActionHom.instCoeTCMulActionHom {X : Type u_2} {Y : Type u_3} {M : Type u_5} {F : Type u_16} [SMul M X] [SMul M Y] [FunLike F X Y] [SMulHomClass F M X Y] :
CoeTC F (X →[M] Y)

Any type satisfying SMulHomClass can be cast into MulActionHom via SMulHomClass.toMulActionHom.

Equations
  • MulActionHom.instCoeTCMulActionHom = { coe := SMulHomClass.toMulActionHom }
theorem IsScalarTower.smulHomClass (M' : Type u_1) (X : Type u_2) [SMul M' X] (Y : Type u_3) [SMul M' Y] (F : Type u_16) [MulOneClass X] [SMul X Y] [IsScalarTower M' X Y] [FunLike F X Y] [SMulHomClass F X X Y] :
SMulHomClass F M' X Y

If Y/X/M forms a scalar tower, any map X → Y preserving X-action also preserves M-action.

theorem MulActionHom.map_smul {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) (m : M') (x : X) :
f (m x) = m f x
theorem MulActionHom.ext {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} :
(∀ (x : X), f x = g x)f = g
theorem MulActionHom.ext_iff {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} :
f = g ∀ (x : X), f x = g x
theorem MulActionHom.congr_fun {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {f : X →[M'] Y} {g : X →[M'] Y} (h : f = g) (x : X) :
f x = g x
def MulActionHom.id (M' : Type u_1) {X : Type u_2} [SMul M' X] :
X →[M'] X

The identity map as an equivariant map.

Equations
@[simp]
theorem MulActionHom.id_apply (M' : Type u_1) {X : Type u_2} [SMul M' X] (x : X) :
def MulActionHom.comp {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {Z : Type u_4} [SMul M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) :
X →[M'] Z

Composition of two equivariant maps.

Equations
@[simp]
theorem MulActionHom.comp_apply {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] {Z : Type u_4} [SMul M' Z] (g : Y →[M'] Z) (f : X →[M'] Y) (x : X) :
(MulActionHom.comp g f) x = g (f x)
@[simp]
theorem MulActionHom.id_comp {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) :
@[simp]
theorem MulActionHom.comp_id {M' : Type u_1} {X : Type u_2} [SMul M' X] {Y : Type u_3} [SMul M' Y] (f : X →[M'] Y) :
@[simp]
theorem MulActionHom.inverse_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →[M] B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
∀ (a : B), (MulActionHom.inverse f g h₁ h₂) a = g a
def MulActionHom.inverse {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →[M] B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
B →[M] A

The inverse of a bijective equivariant map is equivariant.

Equations
@[simp]
theorem SMulCommClass.toMulActionHom_apply {M : Type u_18} (N : Type u_16) (α : Type u_17) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) :
∀ (x : α), (SMulCommClass.toMulActionHom N α c) x = c x
def SMulCommClass.toMulActionHom {M : Type u_18} (N : Type u_16) (α : Type u_17) [SMul M α] [SMul N α] [SMulCommClass M N α] (c : M) :
α →[N] α

If actions of M and N on α commute, then for c : M, (c • · : α → α) is an N-action homomorphism.

Equations
@[reducible]
abbrev DistribMulActionHom.toAddMonoidHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (self : A →+[M] B) :
A →+ B

Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism.

Equations

Equivariant additive monoid homomorphisms.

Equations
  • One or more equations did not get rendered due to their size.
class DistribMulActionHomClass (F : Type u_16) (M : outParam (Type u_17)) (A : outParam (Type u_18)) (B : outParam (Type u_19)) [Monoid M] [AddMonoid A] [AddMonoid B] [DistribMulAction M A] [DistribMulAction M B] [FunLike F A B] extends SMulHomClass , AddMonoidHomClass :

DistribMulActionHomClass F M A B states that F is a type of morphisms preserving the additive monoid structure and scalar multiplication by M.

You should extend this class when you extend DistribMulActionHom.

    Instances
    Equations
    def DistribMulActionHomClass.toDistribMulActionHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {F : Type u_16} [FunLike F A B] [DistribMulActionHomClass F M A B] (f : F) :
    A →+[M] B

    Turn an element of a type F satisfying SMulHomClass F M X Y into an actual MulActionHom. This is declared as the default coercion from F to MulActionHom M X Y.

    Equations
    • f = let __src := f; let __src_1 := f; { toMulActionHom := { toFun := __src.toFun, map_smul' := }, map_zero' := , map_add' := }
    instance DistribMulActionHom.instCoeTCDistribMulActionHom {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {F : Type u_16} [FunLike F A B] [DistribMulActionHomClass F M A B] :
    CoeTC F (A →+[M] B)

    Any type satisfying SMulHomClass can be cast into MulActionHom via SMulHomClass.toMulActionHom.

    Equations
    • DistribMulActionHom.instCoeTCDistribMulActionHom = { coe := DistribMulActionHomClass.toDistribMulActionHom }
    @[simp]
    theorem DistribMulActionHom.toFun_eq_coe {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) :
    f.toFun = f
    theorem DistribMulActionHom.coe_fn_coe {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) :
    f = f
    theorem DistribMulActionHom.coe_fn_coe' {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) :
    f = f
    theorem DistribMulActionHom.ext {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} :
    (∀ (x : A), f x = g x)f = g
    theorem DistribMulActionHom.ext_iff {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} :
    f = g ∀ (x : A), f x = g x
    theorem DistribMulActionHom.congr_fun {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) (x : A) :
    f x = g x
    theorem DistribMulActionHom.toMulActionHom_injective {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) :
    f = g
    theorem DistribMulActionHom.toAddMonoidHom_injective {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {f : A →+[M] B} {g : A →+[M] B} (h : f = g) :
    f = g
    theorem DistribMulActionHom.map_zero {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) :
    f 0 = 0
    theorem DistribMulActionHom.map_add {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (x : A) (y : A) :
    f (x + y) = f x + f y
    theorem DistribMulActionHom.map_neg {M : Type u_5} [Monoid M] (A' : Type u_7) [AddGroup A'] [DistribMulAction M A'] (B' : Type u_9) [AddGroup B'] [DistribMulAction M B'] (f : A' →+[M] B') (x : A') :
    f (-x) = -f x
    theorem DistribMulActionHom.map_sub {M : Type u_5} [Monoid M] (A' : Type u_7) [AddGroup A'] [DistribMulAction M A'] (B' : Type u_9) [AddGroup B'] [DistribMulAction M B'] (f : A' →+[M] B') (x : A') (y : A') :
    f (x - y) = f x - f y
    theorem DistribMulActionHom.map_smul {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (m : M) (x : A) :
    f (m x) = m f x
    def DistribMulActionHom.id (M : Type u_5) [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] :
    A →+[M] A

    The identity map as an equivariant additive monoid homomorphism.

    Equations
    @[simp]
    theorem DistribMulActionHom.id_apply (M : Type u_5) [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] (x : A) :
    Equations
    • DistribMulActionHom.instZeroDistribMulActionHom = { zero := let __src := 0; { toMulActionHom := { toFun := __src.toFun, map_smul' := }, map_zero' := , map_add' := } }
    Equations
    @[simp]
    theorem DistribMulActionHom.coe_zero {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] :
    0 = 0
    @[simp]
    theorem DistribMulActionHom.coe_one {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] :
    1 = id
    theorem DistribMulActionHom.zero_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (a : A) :
    0 a = 0
    theorem DistribMulActionHom.one_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] (a : A) :
    1 a = a
    Equations
    • DistribMulActionHom.instInhabitedDistribMulActionHom = { default := 0 }
    def DistribMulActionHom.comp {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {C : Type u_10} [AddMonoid C] [DistribMulAction M C] (g : B →+[M] C) (f : A →+[M] B) :
    A →+[M] C

    Composition of two equivariant additive monoid homomorphisms.

    Equations
    @[simp]
    theorem DistribMulActionHom.comp_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] {C : Type u_10} [AddMonoid C] [DistribMulAction M C] (g : B →+[M] C) (f : A →+[M] B) (x : A) :
    (DistribMulActionHom.comp g f) x = g (f x)
    @[simp]
    theorem DistribMulActionHom.inverse_apply {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    ∀ (a : B), (DistribMulActionHom.inverse f g h₁ h₂) a = g a
    def DistribMulActionHom.inverse {M : Type u_5} [Monoid M] {A : Type u_6} [AddMonoid A] [DistribMulAction M A] {B : Type u_8} [AddMonoid B] [DistribMulAction M B] (f : A →+[M] B) (g : BA) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    B →+[M] A

    The inverse of a bijective DistribMulActionHom is a DistribMulActionHom.

    Equations
    • One or more equations did not get rendered due to their size.
    theorem DistribMulActionHom.ext_ring {M' : Type u_1} {R : Type u_11} [Semiring R] [AddMonoid M'] [DistribMulAction R M'] {f : R →+[R] M'} {g : R →+[R] M'} (h : f 1 = g 1) :
    f = g
    theorem DistribMulActionHom.ext_ring_iff {M' : Type u_1} {R : Type u_11} [Semiring R] [AddMonoid M'] [DistribMulAction R M'] {f : R →+[R] M'} {g : R →+[R] M'} :
    f = g f 1 = g 1
    @[simp]
    theorem SMulCommClass.toDistribMulActionHom_apply {M : Type u_18} (N : Type u_16) (A : Type u_17) [Monoid N] [AddMonoid A] [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) :
    ∀ (x : A), (SMulCommClass.toDistribMulActionHom N A c) x = c x
    def SMulCommClass.toDistribMulActionHom {M : Type u_18} (N : Type u_16) (A : Type u_17) [Monoid N] [AddMonoid A] [DistribSMul M A] [DistribMulAction N A] [SMulCommClass M N A] (c : M) :
    A →+[N] A

    If DistribMulAction of M and N on A commute, then for each c : M, (c • ·) is an N-action additive homomorphism.

    Equations
    • One or more equations did not get rendered due to their size.
    structure MulSemiringActionHom (M : Type u_5) [Monoid M] (R : Type u_11) [Semiring R] [MulSemiringAction M R] (S : Type u_13) [Semiring S] [MulSemiringAction M S] extends DistribMulActionHom :
    Type (max u_11 u_13)

    Equivariant ring homomorphisms.

    • toFun : RS
    • map_smul' : ∀ (m : M) (x : R), self.toFun (m x) = m self.toFun x
    • map_zero' : self.toFun 0 = 0
    • map_add' : ∀ (x y : R), self.toFun (x + y) = self.toFun x + self.toFun y
    • map_one' : self.toFun 1 = 1

      The proposition that the function preserves 1

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

      The proposition that the function preserves multiplication

    Instances For
    @[reducible]
    abbrev MulSemiringActionHom.toRingHom {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (self : R →+*[M] S) :
    R →+* S

    Reinterpret an equivariant ring homomorphism as a ring homomorphism.

    Equations
    • MulSemiringActionHom.toRingHom self = { toMonoidHom := { toOneHom := { toFun := self.toFun, map_one' := }, map_mul' := }, map_zero' := , map_add' := }

    Equivariant ring homomorphisms.

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

    MulSemiringActionHomClass F M R S states that F is a type of morphisms preserving the ring structure and scalar multiplication by M.

    You should extend this class when you extend MulSemiringActionHom.

      Instances
      Equations
      def MulSemiringActionHomClass.toMulSemiringActionHom {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {F : Type u_16} [FunLike F R S] [MulSemiringActionHomClass F M R S] (f : F) :
      R →+*[M] S

      Turn an element of a type F satisfying MulSemiringActionHomClass F M R S into an actual MulSemiringActionHom. This is declared as the default coercion from F to MulSemiringActionHom M X Y.

      Equations
      • One or more equations did not get rendered due to their size.
      instance MulSemiringActionHom.instCoeTCMulSemiringActionHom {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {F : Type u_16} [FunLike F R S] [MulSemiringActionHomClass F M R S] :
      CoeTC F (R →+*[M] S)

      Any type satisfying MulSemiringActionHomClass can be cast into MulSemiringActionHom via MulSemiringActionHomClass.toMulSemiringActionHom.

      Equations
      • MulSemiringActionHom.instCoeTCMulSemiringActionHom = { coe := MulSemiringActionHomClass.toMulSemiringActionHom }
      theorem MulSemiringActionHom.coe_fn_coe {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) :
      f = f
      theorem MulSemiringActionHom.coe_fn_coe' {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) :
      f = f
      theorem MulSemiringActionHom.ext {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {f : R →+*[M] S} {g : R →+*[M] S} :
      (∀ (x : R), f x = g x)f = g
      theorem MulSemiringActionHom.ext_iff {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {f : R →+*[M] S} {g : R →+*[M] S} :
      f = g ∀ (x : R), f x = g x
      theorem MulSemiringActionHom.map_zero {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) :
      f 0 = 0
      theorem MulSemiringActionHom.map_add {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) (x : R) (y : R) :
      f (x + y) = f x + f y
      theorem MulSemiringActionHom.map_neg {M : Type u_5} [Monoid M] (R' : Type u_12) [Ring R'] [MulSemiringAction M R'] (S' : Type u_14) [Ring S'] [MulSemiringAction M S'] (f : R' →+*[M] S') (x : R') :
      f (-x) = -f x
      theorem MulSemiringActionHom.map_sub {M : Type u_5} [Monoid M] (R' : Type u_12) [Ring R'] [MulSemiringAction M R'] (S' : Type u_14) [Ring S'] [MulSemiringAction M S'] (f : R' →+*[M] S') (x : R') (y : R') :
      f (x - y) = f x - f y
      theorem MulSemiringActionHom.map_one {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) :
      f 1 = 1
      theorem MulSemiringActionHom.map_mul {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) (x : R) (y : R) :
      f (x * y) = f x * f y
      theorem MulSemiringActionHom.map_smul {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] (f : R →+*[M] S) (m : M) (x : R) :
      f (m x) = m f x
      def MulSemiringActionHom.id (M : Type u_5) [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] :
      R →+*[M] R

      The identity map as an equivariant ring homomorphism.

      Equations
      @[simp]
      theorem MulSemiringActionHom.id_apply (M : Type u_5) [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] (x : R) :
      def MulSemiringActionHom.comp {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {T : Type u_15} [Semiring T] [MulSemiringAction M T] (g : S →+*[M] T) (f : R →+*[M] S) :
      R →+*[M] T

      Composition of two equivariant additive monoid homomorphisms.

      Equations
      @[simp]
      theorem MulSemiringActionHom.comp_apply {M : Type u_5} [Monoid M] {R : Type u_11} [Semiring R] [MulSemiringAction M R] {S : Type u_13} [Semiring S] [MulSemiringAction M S] {T : Type u_15} [Semiring T] [MulSemiringAction M T] (g : S →+*[M] T) (f : R →+*[M] S) (x : R) :