feat: port RingTheory.Noetherian (#2976)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
leanprover-community · Mar 20, 2023 · f411c38 · f411c38
1 parent fc708bb
commit f411c38
Show file tree

Hide file tree

Showing 2 changed files with 621 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1291,6 +1291,7 @@ import Mathlib.RingTheory.Multiplicity
 import Mathlib.RingTheory.MvPolynomial.Symmetric
 import Mathlib.RingTheory.MvPolynomial.Tower
 import Mathlib.RingTheory.Nilpotent
+import Mathlib.RingTheory.Noetherian
 import Mathlib.RingTheory.NonZeroDivisors
 import Mathlib.RingTheory.OreLocalization.Basic
 import Mathlib.RingTheory.OreLocalization.OreSet