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