Commit 2025-04-07 05:31 058da7e4

View on Github →

feat(RingTheory): zero-dimensional rings (#21461)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/DualNumber.lean

Modified Mathlib/RingTheory/Extension.lean

Modified Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean

deleted theorem IsLocalization.AtPrime.prime_unique_of_minimal

deleted theorem Localization.AtPrime.nilpotent_iff_mem_maximal_of_minimal

deleted theorem Localization.AtPrime.nilpotent_iff_not_unit_of_minimal

deleted theorem Localization.AtPrime.prime_unique_of_minimal

Modified Mathlib/RingTheory/KrullDimension/Basic.lean

added theorem Ideal.IsPrime.isMaximal'

Created Mathlib/RingTheory/KrullDimension/Zero.lean

added theorem Ideal.jacobson_eq_radical

added theorem IsLocalRing.of_isMaximal_nilradical

added theorem IsLocalization.AtPrime.prime_unique_of_minimal

added theorem Ring.KrullDimLE.eq_maximalIdeal_of_isPrime

added theorem Ring.KrullDimLE.existsUnique_isPrime

added theorem Ring.KrullDimLE.isField_of_isDomain

added theorem Ring.KrullDimLE.isField_of_isReduced

added theorem Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal

added theorem Ring.KrullDimLE.isNilpotent_iff_mem_nonunits

added theorem Ring.KrullDimLE.mem_minimalPrimes_iff

added theorem Ring.KrullDimLE.mem_minimalPrimes_iff_le_of_isPrime

added theorem Ring.KrullDimLE.minimalPrimes_eq_setOf_isMaximal

added theorem Ring.KrullDimLE.minimalPrimes_eq_setOf_isPrime

added theorem Ring.KrullDimLE.nilradical_eq_maximalIdeal

added theorem Ring.KrullDimLE.of_isLocalization

added theorem Ring.KrullDimLE.of_isMaximal_nilradical

added theorem Ring.KrullDimLE.subsingleton_primeSpectrum

added theorem Ring.krullDimLE_zero_and_isLocalRing_tfae

added theorem le_isUnit_iff_zero_not_mem

added theorem ringKrullDimZero_iff_ringKrullDim_eq_zero

Modified Mathlib/RingTheory/LocalProperties/Reduced.lean

Modified Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

added theorem IsLocalRing.isMaximal_iff

modified theorem IsLocalRing.maximal_ideal_unique

deleted theorem IsLocalRing.of_nilradical_isMaximal

Modified Mathlib/RingTheory/Localization/AtPrime.lean

added theorem IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

deleted def PrimeSpectrum.primeSpectrum_unique_of_localization_at_minimal