instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra

English

If R is Noetherian, the substructure (subtype) corresponding to the Rees algebra inside the ambient algebra is of finite type over R.

Русский

Если R — Нетерово кольцо, то подструктура, соответствующая Реес-алгебре внутри окружающей алгебры, имеет конечный тип над R.

LaTeX

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

Lean4

instance [IsNoetherianRing R] : IsNoetherianRing (reesAlgebra I) :=
  Algebra.FiniteType.isNoetherianRing R _

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