instFiniteTypeSubtypePolynomialMemSubalgebraReesAlgebraOfIsNoetherianRing

English

If R is a Noetherian ring, then the Rees algebra of any ideal I is a finitely generated R-algebra (i.e., Noetherian).

Русский

Если R — кольцо Нетер, то Реес-алгебра любого идеала I конечного типа над R (нетеритный).

LaTeX

$$$\text{If } R\text{ is Noetherian, then } \mathrm{reesAlgebra}(I)\text{ is a Noetherian ring (finite type over } R).$$$

Lean4

instance [IsNoetherianRing R] : Algebra.FiniteType R (reesAlgebra I) :=
  ⟨(reesAlgebra I).fg_top.mpr (reesAlgebra.fg <| IsNoetherian.noetherian I)⟩

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