isNoetherianRing_of_fg — Mathlib

English

Let R be a Noetherian ring and S be a finitely generated R-subalgebra of A. Then S is Noetherian as a ring.

Русский

Пусть R — кольцо Неттер, и S — конечнопорождённая подалгебра R в A. Тогда S является Неттеровым кольцом.

LaTeX

$$$\\text{IsNoetherianRing}(S)$$$

Lean4

theorem isNoetherianRing_of_fg {S : Subalgebra R A} (HS : S.FG) [IsNoetherianRing R] : IsNoetherianRing S :=
  let ⟨t, ht⟩ := HS
  ht ▸ (Algebra.adjoin_eq_range R (↑t : Set A)).symm ▸ AlgHom.isNoetherianRing_range _

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