feat: port RingTheory.Valuation.Basic (#2846)

Co-authored-by: Matthew Ballard <matt@mrb.email>
leanprover-community · Mar 17, 2023 · a9138cd · a9138cd
1 parent 27f3e68
commit a9138cd
Show file tree

Hide file tree

Showing 2 changed files with 928 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1274,6 +1274,7 @@ import Mathlib.RingTheory.Subring.Basic
 import Mathlib.RingTheory.Subring.Pointwise
 import Mathlib.RingTheory.Subsemiring.Basic
 import Mathlib.RingTheory.Subsemiring.Pointwise
+import Mathlib.RingTheory.Valuation.Basic
 import Mathlib.SetTheory.Cardinal.Basic
 import Mathlib.SetTheory.Cardinal.Cofinality
 import Mathlib.SetTheory.Cardinal.Continuum