is_noetherian_subring_closure — Mathlib

English

If s is a finite subset of R, then the subring of R generated by s, i.e., Subring.closure s, is Noetherian.

Русский

Пусть s — конечный подмножество кольца R. Подкольцо, порождаемое s, то есть Subring.closure s, является кольцом Неттерa.

LaTeX

$$$\\operatorname{IsNoetherianRing}(\\operatorname{Subring.closure}(s))$$$

Lean4

theorem is_noetherian_subring_closure (s : Set R) (hs : s.Finite) : IsNoetherianRing (Subring.closure s) :=
  show IsNoetherianRing (subalgebraOfSubring (Subring.closure s)) from
    Algebra.adjoin_int s ▸ isNoetherianRing_of_fg (Subalgebra.fg_def.2 ⟨s, hs, rfl⟩)

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