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.

Estimated changes