Commit 2025-01-15 12:34 59c1bde0
View on Github →refactor: split RingTheory/{Prime,Maximal}Spectrum
into RingTheory/Spectrum/{Prime,Maximal}/{Defs,Basic}
(#20772)
Split off definitions of maximal and prime spectrum of a ring to be able to use it in other modules without pulling unnecessary imports.