Commit 2024-03-14 18:30 415f2144

View on Github →

feat(RingTheory/Localization): add facts about localization at minimal prime ideals (#11201) Show that localization at minimal primes results in rings with only a single prime ideal, implying that every non-unit element is nilpotent.

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added def PrimeSpectrum.primeSpectrum_unique_of_localization_at_minimal

Modified Mathlib/RingTheory/Ideal/MinimalPrime.lean

added theorem IsLocalization.AtPrime.prime_unique_of_minimal

added theorem Localization.AtPrime.nilpotent_iff_mem_maximal_of_minimal

added theorem Localization.AtPrime.nilpotent_iff_not_unit_of_minimal

added theorem Localization.AtPrime.prime_unique_of_minimal

Modified Mathlib/RingTheory/Localization/AtPrime.lean

added def IsLocalization.AtPrime.orderIsoOfPrime