THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file proves additional properties of the prime spectrum a ring is Noetherian.
In a noetherian ring, every ideal contains a product of prime ideals ([samuel, § 3.3, Lemma 3])
In a noetherian integral domain which is not a field, every non-zero ideal contains a non-zero product of prime ideals; in a field, the whole ring is a non-zero ideal containing only 0 as product or prime ideals ([samuel, § 3.3, Lemma 3])