English
Let a finite index set be ι and M_i be R-modules. Then the product ∀i, M_i is finite over R if and only if every M_i is finite over R.
Русский
Пусть множество индексов ι конечно; модули M_i. Тогда произведение M_i по ifinite над R эквивалентно тому, что каждый M_i конечен над R.
LaTeX
$$$\\forall \\{M_i : i \\in ι\\},\\; [\\text{Finite } ι]\\; [\\forall i, \\text{Module } R (M_i)]\\;\\bigl(\\text{Module.Finite } R (\\prod_{i \\in ι} M_i) \\Leftrightarrow \\forall i, \\text{Module.Finite } R (M_i)\\bigr)$$
Lean4
instance pi {ι : Type*} {M : ι → Type*} [_root_.Finite ι] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
[h : ∀ i, Module.Finite R (M i)] : Module.Finite R (∀ i, M i) :=
⟨by
rw [← Submodule.pi_top]
exact Submodule.fg_pi fun i => (h i).1⟩
