∀ {R : Type u_2} [inst : CommSemiring R] {N' : Type u_3} [inst_1 : AddCommMonoid N'] [inst_2 : Module R N']
  (Rₛ : Type u_1) [inst_3 : CommSemiring Rₛ] [inst_4 : Algebra R Rₛ] [inst_5 : Module Rₛ N'] [IsScalarTower R Rₛ N'],
  SMulCommClass Rₛ R N'