Commit 2026-04-17 19:17 d16f6345

View on Github →

feat(RingTheory/Spectrum): upgrade toPiLocalization to an AlgEquiv (#38031) This PR upgrades the existing toPiLocalization for prime ideals and maximal ideals to AlgEquivs.

Estimated changes

Modified Mathlib/RingTheory/Spectrum/Maximal/Localization.lean

modified def MaximalSpectrum.toPiLocalization

modified def PrimeSpectrum.piLocalizationToMaximal

modified def PrimeSpectrum.toPiLocalization

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

added theorem MaximalSpectrum.toPiLocalizationEquiv_apply

added theorem MaximalSpectrum.toPiLocalizationEquiv_apply_apply

added def PrimeSpectrum.toPiLocalizationEquiv

added theorem PrimeSpectrum.toPiLocalizationEquiv_apply

added theorem PrimeSpectrum.toPiLocalizationEquiv_apply_apply

modified theorem PrimeSpectrum.toPiLocalization_bijective