instIsNoetherianSpecOfOfIsNoetherianRing

English

If R is a Noetherian ring, then the spectrum of R, viewed as a scheme, is Noetherian.

Русский

Если R — кольцо Нётерово, то спектр R, рассматриваемый как схема, является Нётеровой схемой.

LaTeX

$$$\\forall R\\, [\\text{IsNoetherianRing}(R)\\] \\Rightarrow \\text{IsNoetherian}(\\mathrm{Spec}(\\mathrm{CommRingCat.of\\}R))$$$

Lean4

instance {R} [CommRing R] [IsNoetherianRing R] : IsNoetherian <| Spec <| .of R :=
  by
  suffices IsNoetherianRing (CommRingCat.of R) by infer_instance
  assumption

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