instIsNoetherianSpecOfIsNoetherianRingCarrier

English

Let R be a Noetherian ring. Then the affine scheme Spec(R) is Noetherian.

Русский

Пусть R — кольцо Нётерово. Тогда аффиновый схем Spec(R) является Нётеровой схемой.

LaTeX

$$$\\text{If }R\\text{ is Noetherian, then }\\mathrm{Spec}(R)\\text{ is Noetherian.}$$$

Lean4

/-- If `R` is a Noetherian ring, `Spec R` is a Noetherian scheme. -/
instance {R : CommRingCat} [IsNoetherianRing R] : IsNoetherian (Spec R) where

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