instNoetherianSpaceCarrierCarrierCommRingCatSpecOfIsNoetherianRingCarrier

English

If R is a Noetherian ring, then Spec R is a Noetherian topological space.

Русский

Если R — это кольцо Нётеря, то Spec R — это Нетеровское топологическое пространство.

LaTeX

$$$[\text{IsNoetherianRing } R] \Rightarrow \text{NoetherianSpace}(\operatorname{Spec} R).$$$

Lean4

/-- If `R` is a Noetherian ring, `Spec R` is a Noetherian topological space. -/
instance {R : CommRingCat} [IsNoetherianRing R] : NoetherianSpace (Spec R) := by
  convert PrimeSpectrum.instNoetherianSpace (R := R)

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