Commit 2026-04-17 19:17 2ff88980

View on Github →

feat(RingTheory): PrimeSpectrum.sigmaToPi is an open embedding (#38016) In particular, it is a homeomorphism for finite products. From Pi1.

Estimated changes

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

modified def PrimeSpectrum.sigmaToPi

added theorem PrimeSpectrum.sigmaToPi_apply

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

added theorem PrimeSpectrum.comap_evalRingHom_basicOpen

added theorem PrimeSpectrum.isOpenEmbedding_sigmaToPi

added theorem PrimeSpectrum.sigmaToPiHomeo_apply

added theorem PrimeSpectrum.sigmaToPi_mk_basicOpen