Theorem PrimeSpectrum.isOpenEmbedding_sigmaToPi

Modification history

2026-04-17 19:17
Mathlib/RingTheory/Spectrum/Prime/Topology.lean
feat(RingTheory): `PrimeSpectrum.sigmaToPi` is an open embedding (#38016) …
Added PrimeSpectrum.isOpenEmbedding_sigmaToPiView on Github →