Additive maps underlying semilinear maps #
Forgetting scalar compatibility commutes with composition of semilinear maps.
@[simp]
theorem
LinearMap.toAddMonoidHom_comp
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
{M : Type u_4}
{N : Type u_5}
{P : Type u_6}
[Semiring R]
[Semiring S]
[Semiring T]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module S N]
[Module T P]
{σ : R →+* S}
{τ : S →+* T}
{υ : R →+* T}
[RingHomCompTriple σ τ υ]
(g : N →ₛₗ[τ] P)
(f : M →ₛₗ[σ] N)
:
The additive map underlying a composite is the composite of the underlying additive maps.