English
If ι is a finite index set and each M_i is Noetherian, then the product of the family (M_i)_{i∈ι} is Noetherian.
Русский
Если ι конечен и каждый M_i — Noetherian, то произведение всей семейство (M_i)_{i∈ι} — Noetherian.
LaTeX
$$$[Finite ι] \Rightarrow (\forall i, IsNoetherian R (M_i)) \Rightarrow IsNoetherian R (\prod_{i\in ι} M_i)$$$
Lean4
/-- A version of `isNoetherian_pi` for non-dependent functions. We need this instance because
sometimes Lean fails to apply the dependent version in non-dependent settings (e.g., it fails to
prove that `ι → ℝ` is finite dimensional over `ℝ`). -/
instance isNoetherian_pi' [IsNoetherian R M] : IsNoetherian R (ι → M) :=
isNoetherian_pi
