feat: port RingTheory.DiscreteValuationRing.Basic (#4156)

Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
leanprover-community · May 22, 2023 · e8f2fcb · e8f2fcb
1 parent bea2d58
commit e8f2fcb
Show file tree

Hide file tree

Showing 2 changed files with 493 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1892,6 +1892,7 @@ import Mathlib.RingTheory.Congruence
 import Mathlib.RingTheory.Coprime.Basic
 import Mathlib.RingTheory.Coprime.Ideal
 import Mathlib.RingTheory.Coprime.Lemmas
+import Mathlib.RingTheory.DiscreteValuationRing.Basic
 import Mathlib.RingTheory.EisensteinCriterion
 import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.FinitePresentation