Commit 2026-01-22 10:30 5d919d04

refactor(RingTheory/Spectrum/Prime/Noetherian): move finiteness of minimal primes into a separate file (#34226) This PR moves finiteness of minimal primes into a separate file with a more elementary proof that avoids the heavy imports of PrimeSpectrum. The motivation for this was that importing finiteness of minimal primes into RingTheory/Ideal/AssociatedPrime/Basic in #34221 was resulting in +50% imports, which is reduced to +7% after this change.