A multiple tensor product of finitely generated modules is finitely generated #
instance
PiTensorProduct.finite
{R : Type u_1}
[CommRing R]
{ι : Type u_2}
[Finite ι]
{M : ι → Type u_3}
[(i : ι) → AddCommGroup (M i)]
[(i : ι) → Module R (M i)]
[∀ (i : ι), Module.Finite R (M i)]
:
Module.Finite R (PiTensorProduct R fun (i : ι) => M i)