Theorems · Theorem · commutative algebra

IsNoetherianRing.of_isLocalization_maximal

∀ {R : Type u_1} [inst : CommSemiring R] [Finite (MaximalSpectrum R)] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3)
  [inst_2 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)]
  [inst_3 : (P : Ideal R) → [inst_3 : P.IsMaximal] → Algebra R (Rₚ P)]
  [∀ (P : Ideal R) [inst_4 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P],
  (∀ (P : Ideal R) [inst : P.IsMaximal], IsNoetherianRing (Rₚ P)) → IsNoetherianRing R

A semilocal ring R is Noetherian if its localization at every maximal ideal is a Noetherian ring.

Defined in

Mathlib.RingTheory.LocalProperties.Semilocal

Cited by

1 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringFiniteCommSemiringAlgebraIsLocalization.AtPrime