Theorem PrimeSpectrum.toPiLocalizationEquiv_apply_apply

Modification history

2026-04-17 19:17
Mathlib/RingTheory/Spectrum/Prime/Topology.lean
feat(RingTheory/Spectrum): upgrade `toPiLocalization` to an `AlgEquiv` (#38031) …
Added PrimeSpectrum.toPiLocalizationEquiv_apply_applyView on Github →