Def PrimeSpectrum.sigmaToPi

Modification history

2025-02-12 16:16

Mathlib/RingTheory/Spectrum/Prime/Basic.lean

chore(RingTheory/Spectrum/Prime/Basic): move functoriality to its own file (#21498)

Modified PrimeSpectrum.sigmaToPi View on Github →

2024-12-10 08:25

Mathlib/RingTheory/PrimeSpectrum.lean

feat: PrimeSpectrum has DiscreteTopology iff toLocalization is bijective (#19714) …

Added PrimeSpectrum.sigmaToPi View on Github →