instIsNoetherianRingForallOfFinite

English

If ι is finite, then the product of Noetherian rings indexed by ι is Noetherian.

Русский

Если индексированное множество ι конечно, произведение кольцев по индексу ι Ноетерно.

LaTeX

$$$\forall i, IsNoetherianRing(R_i) \Rightarrow IsNoetherianRing(\prod_{i\in ι} R_i)$$$

Lean4

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

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