feat(ring_theory): quotients of a noetherian ring are noetherian (#9449)

Co-authored-by: Anne Baanen <t.baanen@vu.nl>

src/ring_theory/noetherian.lean

@@ -646,8 +646,8 @@ begin
   exact order_embedding.well_founded (submodule.map_subtype.order_embedding N).dual h,
 end
 
-theorem is_noetherian_of_quotient_of_noetherian (R) [ring R] (M) [add_comm_group M] [module R M]
-  (N : submodule R M) (h : is_noetherian R M) : is_noetherian R N.quotient :=
+instance submodule.quotient.is_noetherian {R} [ring R] {M} [add_comm_group M] [module R M]
+  (N : submodule R M) [h : is_noetherian R M] : is_noetherian R N.quotient :=
 begin
   rw is_noetherian_iff_well_founded at h ⊢,
   exact order_embedding.well_founded (submodule.comap_mkq.order_embedding N).dual h,
@@ -663,6 +663,10 @@ begin
   refine (submodule.restrict_scalars_embedding R S M).dual.well_founded h
 end
 
+instance ideal.quotient.is_noetherian_ring {R : Type*} [comm_ring R] [h : is_noetherian_ring R]
+  (I : ideal R) : is_noetherian_ring I.quotient :=
+is_noetherian_ring_iff.mpr $ is_noetherian_of_tower R $ submodule.quotient.is_noetherian _
+
 theorem is_noetherian_of_fg_of_noetherian {R M} [ring R] [add_comm_group M] [module R M]
   (N : submodule R M) [is_noetherian_ring R] (hN : N.fg) : is_noetherian R N :=
 let ⟨s, hs⟩ := hN in