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.