feat: port RingTheory.QuotientNoetherian (#3308)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Mathlib.lean

@@ -1459,6 +1459,7 @@ import Mathlib.RingTheory.Polynomial.Vieta
 import Mathlib.RingTheory.Prime
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.QuotientNilpotent
+import Mathlib.RingTheory.QuotientNoetherian
 import Mathlib.RingTheory.ReesAlgebra
 import Mathlib.RingTheory.RingInvo
 import Mathlib.RingTheory.SimpleModule

Mathlib/RingTheory/QuotientNoetherian.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+
+! This file was ported from Lean 3 source module ring_theory.quotient_noetherian
+! leanprover-community/mathlib commit da420a8c6dd5bdfb85c4ced85c34388f633bc6ff
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.RingTheory.Noetherian
+import Mathlib.RingTheory.QuotientNilpotent
+
+/-!
+# Noetherian quotient rings and quotient modules
+-/
+
+
+instance Ideal.Quotient.isNoetherianRing {R : Type _} [CommRing R] [h : IsNoetherianRing R]
+    (I : Ideal R) : IsNoetherianRing (R ⧸ I) :=
+  have : IsNoetherian R R := by simp_all only -- Porting note: this instance is needed
+  isNoetherianRing_iff.mpr <| isNoetherian_of_tower R <| Submodule.Quotient.isNoetherian _
+#align ideal.quotient.is_noetherian_ring Ideal.Quotient.isNoetherianRing