∀ {R : Type u_4} {R₂ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] (σ₁₂ : R →+* R₂) (N : Type u_3)
  (P₂ : Type u_2) [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P₂] [inst_4 : Module R N] [inst_5 : Module R₂ P₂],
  SMulCommClass R₂ R₂ (N →ₛₗ[σ₁₂] P₂)