∀ {R : Type u_1} [inst : CommSemiring R] {R₂ : Type u_2} (R₃ : Type u_6) (M : Type u_3) (N : Type u_4) (P : Type u_5)
  [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R M] [inst_7 : Module R₂ N] [inst_8 : Module R₃ P] {σ₁₂ : R →+* R₂}
  {σ₁₃ : R →+* R₃} {σ₂₃ : R₂ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (_f _f' : M →ₛₗ[σ₁₂] N),
  LinearMap.lcompₛₗ R₃ P σ₂₃ (_f + _f') = LinearMap.lcompₛₗ R₃ P σ₂₃ _f + LinearMap.lcompₛₗ R₃ P σ₂₃ _f'