of_finite — Mathlib

English

If each R_i is Artinian and the index set ι is finite, then the product ring ∏_i R_i is Artinian.

Русский

Если для каждого i из конечного множества ι кольца R_i артинановы, то произведение ∏_{i∈ι} R_i артинаново.

LaTeX

$$$ [Finite ι] \\Rightarrow (\\forall i, IsArtinianRing (R_i)) \\Rightarrow IsArtinianRing (\\prod_{i} R_i). $$$

Lean4

theorem of_finite (R S) [Ring R] [Ring S] [Module R S] [IsScalarTower R S S] [IsArtinianRing R] [Module.Finite R S] :
    IsArtinianRing S :=
  isArtinian_of_tower R isArtinian_of_fg_of_artinian'

Похожие утверждения