∀ (R : Type u_1) [inst : CommSemiring R] (S : Type u_4) [inst_1 : CommSemiring S] (N : Type u_2)
  [inst_2 : AddCommMonoid N] [inst_3 : Module R N] [inst_4 : Module S N] (ι : Type u_3) [inst_5 : DecidableEq ι] (i : ι)
  (x : S) (x_1 : N), (x • x_1) ⊗ₜ[R] Pi.single i 1 = (x • x_1) ⊗ₜ[R] Pi.single i 1