@[protected, instance]
def
tensor_product.smul_comm_class_left
{R : Type u_1}
[comm_semiring R]
{R' : Type u_2}
[monoid R']
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[add_comm_monoid N]
[module R M]
[module R N]
[distrib_mul_action R' M]
{R'₂ : Type u_9}
[monoid R'₂]
[distrib_mul_action R'₂ M]
[smul_comm_class R R'₂ M]
[smul_comm_class R R' M]
[smul_comm_class R' R'₂ M] :
smul_comm_class R' R'₂ (tensor_product R M N)
smul_comm_class R' R'₂ M implies smul_comm_class R' R'₂ (M ⊗[R] N)