Finiteness of minimal primes

We prove finiteness of minimal primes above an ideal.

This is proved without reference to PrimeSpectrum to avoid heavy imports.

theorem Ideal.finite_minimalPrimes_of_isNoetherianRing (R : Type u_1) [CommSemiring R] [hR : IsNoetherianRing R] (I : Ideal R) : I.minimalPrimes.Finite

theorem minimalPrimes.finite_of_isNoetherianRing (R : Type u_1) [CommSemiring R] [hR : IsNoetherianRing R] : (minimalPrimes R).Finite