English
If each M_i is Artinian over R for a finite index set ι, then the product ∏_i M_i is Artinian.
Русский
Если для конечного множества индексов ι каждый M_i артинанов, то произведение ∏_i M_i артинаново.
LaTeX
$$$(\\forall i, IsArtinian\\ R\\ (M\\ i)) \\Rightarrow IsArtinian\\ R\\ (\\prod_{i \\in ι} M_i)$$$
Lean4
instance isArtinian_pi :
∀ {M : ι → Type*} [Π i, AddCommGroup (M i)] [Π i, Module R (M i)] [∀ i, IsArtinian R (M i)],
IsArtinian R (Π i, M i) :=
by
apply Finite.induction_empty_option _ _ _ ι
· exact fun e h ↦ isArtinian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)
· infer_instance
· exact fun ih ↦ isArtinian_of_linearEquiv (LinearEquiv.piOptionEquivProd R).symm
