∀ {R : Type u_1} [inst : Ring R] {ι : Type u_5} [Finite ι] {M : ι → Type u_6} [inst_2 : (i : ι) → AddCommGroup (M i)]
  [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), IsNoetherian R (M i)], IsNoetherian R ((i : ι) → M i)