(R : Type u_1) →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      {N : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → TensorProduct R M N →ₗ[R] TensorProduct R M N