isNoetherian_Spec — Mathlib

English

For any commutative ring R, the spectrum Spec(R) is Noetherian if and only if R is Noetherian.

Русский

Для любого коммутативного кольца R спектр Spec(R) является Нётеровым тогда и только тогда, когда R является Нётеровым.

LaTeX

$$$\\forall R\\; (IsNoetherian(\\mathrm{Spec}(R)) \\iff IsNoetherianRing(R))$$$

Lean4

/-- `R` is a Noetherian ring if and only if `Spec R` is a Noetherian scheme. -/
theorem isNoetherian_Spec {R : CommRingCat} : IsNoetherian (Spec R) ↔ IsNoetherianRing R :=
  ⟨fun _ => inferInstance, fun _ => inferInstance⟩

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