mathlib3 documentation


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])