feat: port RingTheory.HahnSeries (#4261)

leanprover-community · May 23, 2023 · 178cf0f · 178cf0f
1 parent 9594d4a
commit 178cf0f
Show file tree

Hide file tree

Showing 4 changed files with 1,893 additions and 10 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1937,6 +1937,7 @@ import Mathlib.RingTheory.GradedAlgebra.Basic
 import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
 import Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
 import Mathlib.RingTheory.GradedAlgebra.Radical
+import Mathlib.RingTheory.HahnSeries
 import Mathlib.RingTheory.Henselian
 import Mathlib.RingTheory.Ideal.AssociatedPrime
 import Mathlib.RingTheory.Ideal.Basic

diff --git a/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean b/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
@@ -433,7 +433,7 @@ theorem addVal_uniformizer {ϖ : R} (hϖ : Irreducible ϖ) : addVal R ϖ = 1 :=
     using addVal_def ϖ 1 hϖ 1
 #align discrete_valuation_ring.add_val_uniformizer DiscreteValuationRing.addVal_uniformizer
 
-@[simp]
+--@[simp] Porting note: simp can prove it
 theorem addVal_mul {a b : R} :
     addVal R (a * b) = addVal R a + addVal R b :=
   (addVal R).map_mul _ _