tensor product L(x)[K] _ commutes with arbitrary products if L/K finite

[kbuzzard]

This is the missing sorry in ProdAdicCompletions.baseChangeEquiv. The point is that L=K^n so L (x)[K] (\prod_i A_i) = \prod_i A_i^n. Note that it's not true that tensor products commute with infinite products in general. Perhaps the general statement is something like: if M is a finite R-module then M (x)[R] \prod_i N_i = prod_i (M (x)[R] N_i?

[maddycrim]

claim