Documentation

Mathlib.RingTheory.KrullDimension.Zero

Zero-dimensional rings #

We provide further API for zero-dimensional rings. Basic definitions and lemmas are provided in Mathlib/RingTheory/KrullDimension/Basic.lean.

@[deprecated Ring.KrullDimLE.existsUnique_isPrime (since := "2024-12-20")]
theorem IsLocalization.AtPrime.prime_unique_of_minimal {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] (hMin : I minimalPrimes R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization.AtPrime S I] {J K : Ideal S} [J.IsPrime] [K.IsPrime] :
J = K
@[deprecated Ring.KrullDimLE.eq_maximalIdeal_of_isPrime (since := "2024-12-20")]

Alias of Ring.KrullDimLE.eq_maximalIdeal_of_isPrime.

@[deprecated Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal (since := "2024-12-20")]

Alias of Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal.

@[deprecated Ring.KrullDimLE.isNilpotent_iff_mem_nonunits (since := "2024-12-20")]

Alias of Ring.KrullDimLE.isNilpotent_iff_mem_nonunits.

@[deprecated PrimeSpectrum.unique_of_ringKrullDimLE_zero "Use `PrimeSpectrum.unique_of_ringKrullDimLE_zero` with `Ring.KrullDimLE.of_isLocalization`" (since := "2024-12-20")]

Alias of PrimeSpectrum.unique_of_ringKrullDimLE_zero.

Equations
Instances For
    @[deprecated IsLocalRing.of_isMaximal_nilradical (since := "2024-11-09")]

    Alias of IsLocalRing.of_isMaximal_nilradical.

    @[deprecated IsLocalization.atUnits (since := "2024-12-20")]
    noncomputable def localizationEquivSelfOfNilradicalIsMaximal {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {M : Submonoid R} [h : (nilradical R).IsMaximal] (h' : 0M) [IsLocalization M S] :

    Let S be the localization of a commutative semiring R at a submonoid M that does not contain 0. If the nilradical of R is maximal then there is a R-algebra isomorphism between R and S.

    Equations
    Instances For