theorem TensorProduct.prod_tmul_prod (R : Type u_1) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] {ι : Type u_4} (s : Finset ι) (a : ι → A) (b : ι → B) : (∏ i ∈ s, a i) ⊗ₜ[R] ∏ i ∈ s, b i = ∏ i ∈ s, a i ⊗ₜ[R] b i