instIsArtinianRingForallOfFinite — Mathlib

English

If ι is finite and each R_i is a ring with IsArtinianRing, then the product ∏_i R_i is Artinian.

Русский

Если индексный набор ι конечно, и каждый R_i артинан, то произведение ∏_i R_i артинаново.

LaTeX

$$$ [Finite\\ ι]\\Rightarrow \\forall i, IsArtinianRing (R_i) \\Rightarrow IsArtinianRing (\\prod_i R_i). $$$

Lean4

instance {ι} [Finite ι] :
    ∀ {R : ι → Type*} [Π i, Semiring (R i)] [∀ i, IsArtinianRing (R i)], IsArtinianRing (Π i, R i) :=
  by
  apply Finite.induction_empty_option _ _ _ ι
  · exact fun e h ↦ RingEquiv.isArtinianRing (.piCongrLeft _ e)
  · infer_instance
  · exact fun ih ↦ RingEquiv.isArtinianRing (.symm .piOptionEquivProd)

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