Theorem PrimeSpectrum.toPiLocalization_bijective

Modification history

2026-04-17 19:17
Mathlib/RingTheory/Spectrum/Prime/Topology.lean
feat(RingTheory/Spectrum): upgrade `toPiLocalization` to an `AlgEquiv` (#38031) …
Modified PrimeSpectrum.toPiLocalization_bijectiveView on Github →
2026-01-06 11:03
Mathlib/RingTheory/Spectrum/Prime/Topology.lean
feat(RingTheory): construct etale neighborhood that isolates point in fiber (#32823)
Added PrimeSpectrum.toPiLocalization_bijectiveView on Github →