Strongly Noetherian rings and constructive ideal theory
We give a new constructive definition for Noetherian rings. It has a very concrete statement and is nevertheless strong enough to prove constructively the termination of algorithms involving trees of ideals. The efficiency of such algorithms (at least for providing clear and intuitive constructive proofs) is illustrated in a section about LaskerNoether rings: we give constructive proofs for the existence of the minimal primes over an ideal, of its radical, of its primary decomposition, in a wide class of polynomial rings.
noetherian ring