Abstract

We give a constructive treatment of the theory of Noetherian rings. We avoid the usual restriction to coherent rings; we can even deal with non-discrete rings. We introduce the concept of rings with certifiable equality which covers discrete rings and much more. A ring R with certifiable equality can be fitted with a partial ideal membership test for ideals of R. Lazy bases of ideals of R [X ] are introduced in order to derive a partial ideal membership test for ideals of R [X ]. It is then proved that if R is Noetherian, then so is R [X ]