From 266ef1ba04efda8ba83052916c251e302b86b4dc Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Tue, 28 Apr 2026 16:30:20 +0200
Subject: [PATCH 01/14] add lemmas to RingTheory.DedekindDomain.Factorization

---
 .../DedekindDomain/Factorization.lean         | 137 ++++++++++++++++++
 1 file changed, 137 insertions(+)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index f19e75dd949380..cab022dc764fb2 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.NumberTheory.RamificationInertia.Basic
 public import Mathlib.Order.Filter.Cofinite
+public import Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
 
 /-!
 # Factorization of ideals and fractional ideals of Dedekind domains
@@ -842,3 +843,139 @@ theorem Ideal.map_algebraMap_eq_finsetProd_pow {p : Ideal S} [p.IsMaximal] (hp :
 alias Ideal.map_algebraMap_eq_finset_prod_pow := Ideal.map_algebraMap_eq_finsetProd_pow
 
 end primesOver
+
+/-!
+### Conversion between various multplicities
+-/
+
+section conversion
+
+variable {R : Type*} [CommRing R] [IsDedekindDomain R]
+
+namespace IsDedekindDomain.HeightOneSpectrum
+
+open UniqueFactorizationMonoid in
+/-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
+as `multiplicity p.asIdeal I`. -/
+@[simp]
+lemma count_normalizedFactors_eq_multiplicity [DecidableEq (Ideal R)] {I : Ideal R} (hI : I ≠ ⊥)
+    (p : HeightOneSpectrum R) :
+    Multiset.count p.asIdeal (normalizedFactors I) = multiplicity p.asIdeal I := by
+  have := emultiplicity_eq_count_normalizedFactors (irreducible p) hI
+  rw [normalize_eq p.asIdeal] at this
+  apply_fun ((↑) : ℕ → ℕ∞) using CharZero.cast_injective
+  rw [← this]
+  exact (finiteMultiplicity_of_emultiplicity_eq_natCast this).emultiplicity_eq_multiplicity
+
+/-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
+as `multiplicity p.asIdeal I`. -/
+@[simp]
+lemma maxPowDividing_eq_pow_multiplicity {I : Ideal R} (hI : I ≠ ⊥) (p : HeightOneSpectrum R) :
+    p.maxPowDividing I = p.asIdeal ^ multiplicity p.asIdeal I := by
+  classical
+  rw [maxPowDividing_eq_pow_multiset_count _ hI, count_normalizedFactors_eq_multiplicity hI]
+
+/-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
+as `multiplicity p.asIdeal I`. -/
+@[simp]
+lemma factorization_eq_multiplicity {I : Ideal R} (hI : I ≠ ⊥) (p : HeightOneSpectrum R) :
+    factorization I p.asIdeal = multiplicity p.asIdeal I := by
+  rw [factorization_eq_count, count_normalizedFactors_eq_multiplicity hI]
+
+end IsDedekindDomain.HeightOneSpectrum
+
+end conversion
+
+/-!
+### Lemmas about multiplicities
+
+We collect here lemmas about the multiplicity of a prime ideal `p` in the factorization
+of some ideal `I`.
+These are phrased in terms of `multiplicity p.asIdeal I`.
+-/
+
+section multiplicity
+
+variable {R : Type*} [CommRing R] [IsDedekindDomain R]
+
+lemma Ideal.finprod_heightOneSpectrum_pow_multiplicity {I : Ideal R} (hI : I ≠ ⊥) :
+    ∏ᶠ p : HeightOneSpectrum R, p.asIdeal ^ multiplicity p.asIdeal I = I := by
+  simpa only [maxPowDividing_eq_pow_multiplicity hI]
+    using finprod_heightOneSpectrum_factorization hI
+
+namespace IsDedekindDomain.HeightOneSpectrum
+
+lemma multiplicity_le_of_ideal_ge (p : HeightOneSpectrum R) {I J : Ideal R} (h : J ≤ I)
+    (hJ : J ≠ ⊥) :
+    multiplicity p.asIdeal I ≤ multiplicity p.asIdeal J := by
+  classical
+  rw [← count_normalizedFactors_eq_multiplicity hJ,
+    ← count_normalizedFactors_eq_multiplicity <| ne_bot_of_le_ne_bot hJ h]
+  exact Ideal.count_le_of_ideal_ge h hJ _
+
+open UniqueFactorizationMonoid Multiset in
+lemma multiplicity_sup (p : HeightOneSpectrum R) {I J : Ideal R} (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
+    multiplicity p.asIdeal (I ⊔ J) = multiplicity p.asIdeal I ⊓ multiplicity p.asIdeal J := by
+  classical
+  rw [Ideal.sup_eq_prod_inf_factors hI hJ, ← count_normalizedFactors_eq_multiplicity ?h,
+    ← count_normalizedFactors_eq_multiplicity hI, ← count_normalizedFactors_eq_multiplicity hJ]
+  -- extracted from the proof of `sup_eq_prod_inf_factors`
+  --   ==> refactor that (Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas)
+  case h =>
+    exact prod_ne_zero_of_prime _
+      fun _ h ↦ prime_of_normalized_factor _ (mem_inter.mp h).1
+  have H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod =
+      normalizedFactors I ∩ normalizedFactors J := by
+    refine normalizedFactors_prod_of_prime fun p hp ↦ ?_
+    rw [Multiset.mem_inter] at hp
+    exact prime_of_normalized_factor p hp.left
+  rw [H]
+  exact count_inter ..
+
+lemma emultiplicity_sup (p : HeightOneSpectrum R) (I J : Ideal R) :
+    emultiplicity p.asIdeal (I ⊔ J) = emultiplicity p.asIdeal I ⊓ emultiplicity p.asIdeal J := by
+  rcases eq_or_ne I ⊥ with rfl | hI
+  · rw [bot_eq_zero, emultiplicity_zero]
+    simp
+  rcases eq_or_ne J ⊥ with rfl | hJ
+  · rw [bot_eq_zero, emultiplicity_zero]
+    simp
+  have : I ⊔ J ≠ ⊥ := by grind
+  have H {I' : Ideal R} (h : I' ≠ ⊥) : FiniteMultiplicity p.asIdeal I' :=
+    FiniteMultiplicity.of_prime_left (prime p) h
+  rw [(H this).emultiplicity_eq_multiplicity, (H hI).emultiplicity_eq_multiplicity,
+    (H hJ).emultiplicity_eq_multiplicity, multiplicity_sup _ hI hJ]
+  norm_cast
+
+lemma emultiplicity_ciSup {ι : Type*} [Finite ι] (p : HeightOneSpectrum R) (I : ι → Ideal R) :
+    emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i) := by
+  induction ι using Finite.induction_empty_option with
+  | h_empty =>
+    rw [iSup_of_empty, iInf_of_empty]
+    exact emultiplicity_zero _
+  | of_equiv e ih =>
+    specialize @ih (I ∘ e)
+    rw [← sSup_range, ← sInf_range] at ih ⊢
+    rw [EquivLike.range_comp I e] at ih
+    rw [ih, ← EquivLike.range_comp (fun i ↦ emultiplicity p.asIdeal (I i)) e]
+    rfl
+  | h_option ih =>
+    rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
+
+lemma multiplicity_ciSup {ι : Type*} [Finite ι] [Nonempty ι] (p : HeightOneSpectrum R)
+    {I : ι → Ideal R} (hI : ∀ i, I i ≠ ⊥) :
+    multiplicity p.asIdeal (⨆ i, I i) = ⨅ i, multiplicity p.asIdeal (I i) := by
+  have H i : FiniteMultiplicity p.asIdeal (I i) :=
+    FiniteMultiplicity.of_prime_left (prime p) <| hI i
+  have H' : FiniteMultiplicity p.asIdeal (⨆ i, I i) := by
+    refine FiniteMultiplicity.of_prime_left (prime p) ?_
+    contrapose! hI
+    rw [← bot_eq_zero, iSup_eq_bot] at hI
+    exact ⟨Classical.ofNonempty, hI _⟩
+  have := emultiplicity_ciSup p I
+  simp only [H'.emultiplicity_eq_multiplicity, (H _).emultiplicity_eq_multiplicity] at this
+  exact_mod_cast this
+
+end IsDedekindDomain.HeightOneSpectrum
+
+end multiplicity

From bb4ebf518c3e85a1c6ee7918ccae28db0a5cb15b Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Tue, 28 Apr 2026 16:49:14 +0200
Subject: [PATCH 02/14] extract lemmas from Ideal.sup_eq_prod_inf_factors

---
 .../DedekindDomain/Factorization.lean         | 15 +-----
 .../DedekindDomain/Ideal/Lemmas.lean          | 49 +++++++++++--------
 2 files changed, 30 insertions(+), 34 deletions(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index cab022dc764fb2..1af4e635b3bb26 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -908,7 +908,6 @@ namespace IsDedekindDomain.HeightOneSpectrum
 lemma multiplicity_le_of_ideal_ge (p : HeightOneSpectrum R) {I J : Ideal R} (h : J ≤ I)
     (hJ : J ≠ ⊥) :
     multiplicity p.asIdeal I ≤ multiplicity p.asIdeal J := by
-  classical
   rw [← count_normalizedFactors_eq_multiplicity hJ,
     ← count_normalizedFactors_eq_multiplicity <| ne_bot_of_le_ne_bot hJ h]
   exact Ideal.count_le_of_ideal_ge h hJ _
@@ -916,20 +915,10 @@ lemma multiplicity_le_of_ideal_ge (p : HeightOneSpectrum R) {I J : Ideal R} (h :
 open UniqueFactorizationMonoid Multiset in
 lemma multiplicity_sup (p : HeightOneSpectrum R) {I J : Ideal R} (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
     multiplicity p.asIdeal (I ⊔ J) = multiplicity p.asIdeal I ⊓ multiplicity p.asIdeal J := by
-  classical
   rw [Ideal.sup_eq_prod_inf_factors hI hJ, ← count_normalizedFactors_eq_multiplicity ?h,
     ← count_normalizedFactors_eq_multiplicity hI, ← count_normalizedFactors_eq_multiplicity hJ]
-  -- extracted from the proof of `sup_eq_prod_inf_factors`
-  --   ==> refactor that (Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas)
-  case h =>
-    exact prod_ne_zero_of_prime _
-      fun _ h ↦ prime_of_normalized_factor _ (mem_inter.mp h).1
-  have H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod =
-      normalizedFactors I ∩ normalizedFactors J := by
-    refine normalizedFactors_prod_of_prime fun p hp ↦ ?_
-    rw [Multiset.mem_inter] at hp
-    exact prime_of_normalized_factor p hp.left
-  rw [H]
+  case h => exact Ideal.prod_inter_normalizedFactors_ne_zero I J
+  rw [Ideal.normalizedFactors_prod_inter_eq_inter]
   exact count_inter ..
 
 lemma emultiplicity_sup (p : HeightOneSpectrum R) (I J : Ideal R) :
diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
index 351c7bb96a9ea4..fb4bf85e621dc3 100644
--- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
@@ -399,33 +399,40 @@ theorem count_le_of_ideal_ge
 
 @[deprecated (since := "2026-04-16")] alias _root_.count_le_of_ideal_ge := count_le_of_ideal_ge
 
+variable (I J) in
+lemma normalizedFactors_prod_inter_eq_inter :
+    normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod =
+      normalizedFactors I ∩ normalizedFactors J := by
+  apply normalizedFactors_prod_of_prime
+  intro p hp
+  rw [mem_inter] at hp
+  exact prime_of_normalized_factor p hp.left
+
+variable (I J) in
+lemma prod_inter_normalizedFactors_ne_zero :
+    (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0 :=
+  Multiset.prod_ne_zero_of_prime (normalizedFactors I ∩ normalizedFactors J)
+    fun _ h ↦ prime_of_normalized_factor _ (Multiset.mem_inter.1 h).1
+
 theorem sup_eq_prod_inf_factors (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
     I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod := by
-  have H : normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod =
-      normalizedFactors I ∩ normalizedFactors J := by
-    apply normalizedFactors_prod_of_prime
-    intro p hp
-    rw [mem_inter] at hp
-    exact prime_of_normalized_factor p hp.left
-  have := Multiset.prod_ne_zero_of_prime (normalizedFactors I ∩ normalizedFactors J) fun _ h =>
-      prime_of_normalized_factor _ (Multiset.mem_inter.1 h).1
+  have := prod_inter_normalizedFactors_ne_zero I J
   apply le_antisymm
   · rw [sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
-    constructor
-    · rw [dvd_iff_normalizedFactors_le_normalizedFactors this hI, H]
-      exact inf_le_left
-    · rw [dvd_iff_normalizedFactors_le_normalizedFactors this hJ, H]
-      exact inf_le_right
-  · rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors,
-      normalizedFactors_prod_of_prime, le_iff_count]
-    · intro a
-      rw [Multiset.count_inter]
-      exact le_min (count_le_of_ideal_ge le_sup_left hI a) (count_le_of_ideal_ge le_sup_right hJ a)
-    · intro p hp
+    constructor <;>
+      rw [dvd_iff_normalizedFactors_le_normalizedFactors this (by assumption),
+        normalizedFactors_prod_inter_eq_inter]
+    exacts [inf_le_left, inf_le_right]
+  · rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors ?H₁ this,
+      normalizedFactors_prod_of_prime ?H₂, le_iff_count]
+    case H₁ => exact ne_bot_of_le_ne_bot hI le_sup_left
+    case H₂ =>
+      intro p hp
       rw [mem_inter] at hp
       exact prime_of_normalized_factor p hp.left
-    · exact ne_bot_of_le_ne_bot hI le_sup_left
-    · exact this
+    intro a
+    rw [Multiset.count_inter]
+    exact le_min (count_le_of_ideal_ge le_sup_left hI a) (count_le_of_ideal_ge le_sup_right hJ a)
 
 @[deprecated (since := "2026-04-16")]
 alias _root_.sup_eq_prod_inf_factors := sup_eq_prod_inf_factors

From 397d1b295b5fbc7869d48b154f3893fcfe36caac Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Tue, 28 Apr 2026 17:04:10 +0200
Subject: [PATCH 03/14] minor golfing, variables

---
 .../DedekindDomain/Factorization.lean         | 23 +++++++++++--------
 1 file changed, 13 insertions(+), 10 deletions(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index 1af4e635b3bb26..9002c3603e947d 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -905,15 +905,16 @@ lemma Ideal.finprod_heightOneSpectrum_pow_multiplicity {I : Ideal R} (hI : I ≠
 
 namespace IsDedekindDomain.HeightOneSpectrum
 
-lemma multiplicity_le_of_ideal_ge (p : HeightOneSpectrum R) {I J : Ideal R} (h : J ≤ I)
-    (hJ : J ≠ ⊥) :
+variable (p : HeightOneSpectrum R) {I J : Ideal R}
+
+lemma multiplicity_le_of_ideal_ge (h : J ≤ I) (hJ : J ≠ ⊥) :
     multiplicity p.asIdeal I ≤ multiplicity p.asIdeal J := by
   rw [← count_normalizedFactors_eq_multiplicity hJ,
     ← count_normalizedFactors_eq_multiplicity <| ne_bot_of_le_ne_bot hJ h]
   exact Ideal.count_le_of_ideal_ge h hJ _
 
 open UniqueFactorizationMonoid Multiset in
-lemma multiplicity_sup (p : HeightOneSpectrum R) {I J : Ideal R} (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
+lemma multiplicity_sup (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
     multiplicity p.asIdeal (I ⊔ J) = multiplicity p.asIdeal I ⊓ multiplicity p.asIdeal J := by
   rw [Ideal.sup_eq_prod_inf_factors hI hJ, ← count_normalizedFactors_eq_multiplicity ?h,
     ← count_normalizedFactors_eq_multiplicity hI, ← count_normalizedFactors_eq_multiplicity hJ]
@@ -921,7 +922,8 @@ lemma multiplicity_sup (p : HeightOneSpectrum R) {I J : Ideal R} (hI : I ≠ ⊥
   rw [Ideal.normalizedFactors_prod_inter_eq_inter]
   exact count_inter ..
 
-lemma emultiplicity_sup (p : HeightOneSpectrum R) (I J : Ideal R) :
+variable (I J) in
+lemma emultiplicity_sup :
     emultiplicity p.asIdeal (I ⊔ J) = emultiplicity p.asIdeal I ⊓ emultiplicity p.asIdeal J := by
   rcases eq_or_ne I ⊥ with rfl | hI
   · rw [bot_eq_zero, emultiplicity_zero]
@@ -936,23 +938,24 @@ lemma emultiplicity_sup (p : HeightOneSpectrum R) (I J : Ideal R) :
     (H hJ).emultiplicity_eq_multiplicity, multiplicity_sup _ hI hJ]
   norm_cast
 
-lemma emultiplicity_ciSup {ι : Type*} [Finite ι] (p : HeightOneSpectrum R) (I : ι → Ideal R) :
+variable {ι : Type*} [Finite ι]
+
+lemma emultiplicity_ciSup (I : ι → Ideal R) :
     emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i) := by
   induction ι using Finite.induction_empty_option with
   | h_empty =>
     rw [iSup_of_empty, iInf_of_empty]
     exact emultiplicity_zero _
   | of_equiv e ih =>
-    specialize @ih (I ∘ e)
+    specialize ih (I ∘ e)
     rw [← sSup_range, ← sInf_range] at ih ⊢
     rw [EquivLike.range_comp I e] at ih
-    rw [ih, ← EquivLike.range_comp (fun i ↦ emultiplicity p.asIdeal (I i)) e]
-    rfl
+    rw [ih]
+    exact congrArg _ <| EquivLike.range_comp (emultiplicity p.asIdeal <| I ·) e
   | h_option ih =>
     rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
 
-lemma multiplicity_ciSup {ι : Type*} [Finite ι] [Nonempty ι] (p : HeightOneSpectrum R)
-    {I : ι → Ideal R} (hI : ∀ i, I i ≠ ⊥) :
+lemma multiplicity_ciSup [Nonempty ι] {I : ι → Ideal R} (hI : ∀ i, I i ≠ ⊥) :
     multiplicity p.asIdeal (⨆ i, I i) = ⨅ i, multiplicity p.asIdeal (I i) := by
   have H i : FiniteMultiplicity p.asIdeal (I i) :=
     FiniteMultiplicity.of_prime_left (prime p) <| hI i

From 743338b40067fee5c1969a030ef3cef2c3e9d659 Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Tue, 28 Apr 2026 17:08:06 +0200
Subject: [PATCH 04/14] documentation, variables

---
 Mathlib/RingTheory/DedekindDomain/Factorization.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index 9002c3603e947d..893bba9c18cc79 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -846,6 +846,9 @@ end primesOver
 
 /-!
 ### Conversion between various multplicities
+
+We provide some `simp` lemmas that convert various ways of expressing the multiplicity of
+a prime ideal `p` in the factorization of some ideal `I` into `multiplicity p.asIdeal I`.
 -/
 
 section conversion

From c35cfb1a7ea68c70a09796b8d9f12a084c569529 Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Tue, 28 Apr 2026 17:08:15 +0200
Subject: [PATCH 05/14] documentation, variables

---
 Mathlib/RingTheory/DedekindDomain/Factorization.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index 893bba9c18cc79..9799c86c6f1387 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -857,12 +857,14 @@ variable {R : Type*} [CommRing R] [IsDedekindDomain R]
 
 namespace IsDedekindDomain.HeightOneSpectrum
 
+variable {I : Ideal R} (hI : I ≠ ⊥) (p : HeightOneSpectrum R)
+include hI
+
 open UniqueFactorizationMonoid in
 /-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
 as `multiplicity p.asIdeal I`. -/
 @[simp]
-lemma count_normalizedFactors_eq_multiplicity [DecidableEq (Ideal R)] {I : Ideal R} (hI : I ≠ ⊥)
-    (p : HeightOneSpectrum R) :
+lemma count_normalizedFactors_eq_multiplicity :
     Multiset.count p.asIdeal (normalizedFactors I) = multiplicity p.asIdeal I := by
   have := emultiplicity_eq_count_normalizedFactors (irreducible p) hI
   rw [normalize_eq p.asIdeal] at this
@@ -873,7 +875,7 @@ lemma count_normalizedFactors_eq_multiplicity [DecidableEq (Ideal R)] {I : Ideal
 /-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
 as `multiplicity p.asIdeal I`. -/
 @[simp]
-lemma maxPowDividing_eq_pow_multiplicity {I : Ideal R} (hI : I ≠ ⊥) (p : HeightOneSpectrum R) :
+lemma maxPowDividing_eq_pow_multiplicity :
     p.maxPowDividing I = p.asIdeal ^ multiplicity p.asIdeal I := by
   classical
   rw [maxPowDividing_eq_pow_multiset_count _ hI, count_normalizedFactors_eq_multiplicity hI]
@@ -881,7 +883,7 @@ lemma maxPowDividing_eq_pow_multiplicity {I : Ideal R} (hI : I ≠ ⊥) (p : Hei
 /-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
 as `multiplicity p.asIdeal I`. -/
 @[simp]
-lemma factorization_eq_multiplicity {I : Ideal R} (hI : I ≠ ⊥) (p : HeightOneSpectrum R) :
+lemma factorization_eq_multiplicity :
     factorization I p.asIdeal = multiplicity p.asIdeal I := by
   rw [factorization_eq_count, count_normalizedFactors_eq_multiplicity hI]
 

From b5346d7e8daee310f2588263e80a532170f21eb4 Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Tue, 28 Apr 2026 17:24:22 +0200
Subject: [PATCH 06/14] de-simp maxPowDividing_eq_pow_multiplicity

---
 Mathlib/RingTheory/DedekindDomain/Factorization.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index 9799c86c6f1387..2c12bf255cb11b 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -874,7 +874,6 @@ lemma count_normalizedFactors_eq_multiplicity :
 
 /-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
 as `multiplicity p.asIdeal I`. -/
-@[simp]
 lemma maxPowDividing_eq_pow_multiplicity :
     p.maxPowDividing I = p.asIdeal ^ multiplicity p.asIdeal I := by
   classical

From 21183193b00d6eecad37c19413656174b5083a48 Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Tue, 28 Apr 2026 20:22:10 +0200
Subject: [PATCH 07/14] typo, docs, ciSup -> iSup

---
 Mathlib/RingTheory/DedekindDomain/Factorization.lean | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index 2c12bf255cb11b..e55e6f137d43e6 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -845,9 +845,9 @@ alias Ideal.map_algebraMap_eq_finset_prod_pow := Ideal.map_algebraMap_eq_finsetP
 end primesOver
 
 /-!
-### Conversion between various multplicities
+### Conversion between various multiplicities
 
-We provide some `simp` lemmas that convert various ways of expressing the multiplicity of
+We provide some lemmas that convert various ways of expressing the multiplicity of
 a prime ideal `p` in the factorization of some ideal `I` into `multiplicity p.asIdeal I`.
 -/
 
@@ -872,6 +872,8 @@ lemma count_normalizedFactors_eq_multiplicity :
   rw [← this]
   exact (finiteMultiplicity_of_emultiplicity_eq_natCast this).emultiplicity_eq_multiplicity
 
+-- This is not `simp`; otherwise some `aesop` proofs break
+-- in `Mathlib.Algebra.Module.Torsion.PrimaryComponent`.
 /-- Normalize the multiplicity of a prime ideal `p` in the factorization of `I`
 as `multiplicity p.asIdeal I`. -/
 lemma maxPowDividing_eq_pow_multiplicity :
@@ -944,7 +946,7 @@ lemma emultiplicity_sup :
 
 variable {ι : Type*} [Finite ι]
 
-lemma emultiplicity_ciSup (I : ι → Ideal R) :
+lemma emultiplicity_iSup (I : ι → Ideal R) :
     emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i) := by
   induction ι using Finite.induction_empty_option with
   | h_empty =>
@@ -959,7 +961,7 @@ lemma emultiplicity_ciSup (I : ι → Ideal R) :
   | h_option ih =>
     rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
 
-lemma multiplicity_ciSup [Nonempty ι] {I : ι → Ideal R} (hI : ∀ i, I i ≠ ⊥) :
+lemma multiplicity_iSup [Nonempty ι] {I : ι → Ideal R} (hI : ∀ i, I i ≠ ⊥) :
     multiplicity p.asIdeal (⨆ i, I i) = ⨅ i, multiplicity p.asIdeal (I i) := by
   have H i : FiniteMultiplicity p.asIdeal (I i) :=
     FiniteMultiplicity.of_prime_left (prime p) <| hI i
@@ -968,7 +970,7 @@ lemma multiplicity_ciSup [Nonempty ι] {I : ι → Ideal R} (hI : ∀ i, I i ≠
     contrapose! hI
     rw [← bot_eq_zero, iSup_eq_bot] at hI
     exact ⟨Classical.ofNonempty, hI _⟩
-  have := emultiplicity_ciSup p I
+  have := emultiplicity_iSup p I
   simp only [H'.emultiplicity_eq_multiplicity, (H _).emultiplicity_eq_multiplicity] at this
   exact_mod_cast this
 

From 9c3373aad42676f4acd36b1ac5c17a3673f2c083 Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Wed, 29 Apr 2026 14:31:16 +0200
Subject: [PATCH 08/14] suggestion from review

---
 Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
index fb4bf85e621dc3..f1b41804e713fa 100644
--- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
@@ -424,12 +424,8 @@ theorem sup_eq_prod_inf_factors (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
         normalizedFactors_prod_inter_eq_inter]
     exacts [inf_le_left, inf_le_right]
   · rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors ?H₁ this,
-      normalizedFactors_prod_of_prime ?H₂, le_iff_count]
+      normalizedFactors_prod_inter_eq_inter, le_iff_count]
     case H₁ => exact ne_bot_of_le_ne_bot hI le_sup_left
-    case H₂ =>
-      intro p hp
-      rw [mem_inter] at hp
-      exact prime_of_normalized_factor p hp.left
     intro a
     rw [Multiset.count_inter]
     exact le_min (count_le_of_ideal_ge le_sup_left hI a) (count_le_of_ideal_ge le_sup_right hJ a)

From c47e0dd6decbe889c62d5650348fb983d56a6aa4 Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Wed, 29 Apr 2026 14:50:38 +0200
Subject: [PATCH 09/14] generalize extracted lemmas and move to other file

---
 .../DedekindDomain/Ideal/Lemmas.lean          | 19 ++-----------------
 .../NormalizedFactors.lean                    | 18 ++++++++++++++++++
 2 files changed, 20 insertions(+), 17 deletions(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
index f1b41804e713fa..5e4e2ed8417ff3 100644
--- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
@@ -399,21 +399,6 @@ theorem count_le_of_ideal_ge
 
 @[deprecated (since := "2026-04-16")] alias _root_.count_le_of_ideal_ge := count_le_of_ideal_ge
 
-variable (I J) in
-lemma normalizedFactors_prod_inter_eq_inter :
-    normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod =
-      normalizedFactors I ∩ normalizedFactors J := by
-  apply normalizedFactors_prod_of_prime
-  intro p hp
-  rw [mem_inter] at hp
-  exact prime_of_normalized_factor p hp.left
-
-variable (I J) in
-lemma prod_inter_normalizedFactors_ne_zero :
-    (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0 :=
-  Multiset.prod_ne_zero_of_prime (normalizedFactors I ∩ normalizedFactors J)
-    fun _ h ↦ prime_of_normalized_factor _ (Multiset.mem_inter.1 h).1
-
 theorem sup_eq_prod_inf_factors (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
     I ⊔ J = (normalizedFactors I ∩ normalizedFactors J).prod := by
   have := prod_inter_normalizedFactors_ne_zero I J
@@ -423,9 +408,9 @@ theorem sup_eq_prod_inf_factors (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
       rw [dvd_iff_normalizedFactors_le_normalizedFactors this (by assumption),
         normalizedFactors_prod_inter_eq_inter]
     exacts [inf_le_left, inf_le_right]
-  · rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors ?H₁ this,
+  · rw [← dvd_iff_le, dvd_iff_normalizedFactors_le_normalizedFactors ?H this,
       normalizedFactors_prod_inter_eq_inter, le_iff_count]
-    case H₁ => exact ne_bot_of_le_ne_bot hI le_sup_left
+    case H => exact ne_bot_of_le_ne_bot hI le_sup_left
     intro a
     rw [Multiset.count_inter]
     exact le_min (count_le_of_ideal_ge le_sup_left hI a) (count_le_of_ideal_ge le_sup_right hJ a)
diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
index 51460d4784ba57..53b75fbe6e03a7 100644
--- a/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
+++ b/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
@@ -403,3 +403,21 @@ protected noncomputable def normalizationMonoid : NormalizationMonoid α :=
       apply prod_normalizedFactors hx)
 
 end UniqueFactorizationMonoid
+
+namespace UniqueFactorizationMonoid
+
+open  Multiset
+
+variable {α : Type*} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq α]
+
+lemma normalizedFactors_prod_inter_eq_inter [Subsingleton αˣ] (a b : α) :
+    normalizedFactors (normalizedFactors a ∩ normalizedFactors b).prod =
+      normalizedFactors a ∩ normalizedFactors b :=
+  normalizedFactors_prod_of_prime
+    fun _ h ↦ prime_of_normalized_factor _ (mem_inter.mp h).left
+
+lemma prod_inter_normalizedFactors_ne_zero [NormalizationMonoid α] [Nontrivial α] (a b : α) :
+    (normalizedFactors a ∩ normalizedFactors b).prod ≠ 0 :=
+  prod_ne_zero_of_prime _ fun _ h ↦ prime_of_normalized_factor _ (mem_inter.mp h).left
+
+end UniqueFactorizationMonoid

From f9c40cbeff8d7cef3b64a539f6b29a6fde0d553e Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Wed, 29 Apr 2026 15:10:56 +0200
Subject: [PATCH 10/14] fix

---
 Mathlib/RingTheory/DedekindDomain/Factorization.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index e55e6f137d43e6..72caa23824ca89 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -924,8 +924,8 @@ lemma multiplicity_sup (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
     multiplicity p.asIdeal (I ⊔ J) = multiplicity p.asIdeal I ⊓ multiplicity p.asIdeal J := by
   rw [Ideal.sup_eq_prod_inf_factors hI hJ, ← count_normalizedFactors_eq_multiplicity ?h,
     ← count_normalizedFactors_eq_multiplicity hI, ← count_normalizedFactors_eq_multiplicity hJ]
-  case h => exact Ideal.prod_inter_normalizedFactors_ne_zero I J
-  rw [Ideal.normalizedFactors_prod_inter_eq_inter]
+  case h => exact prod_inter_normalizedFactors_ne_zero I J
+  rw [normalizedFactors_prod_inter_eq_inter]
   exact count_inter ..
 
 variable (I J) in

From 0ba6943263958aebf2e8353a0beb0ac7b3a00a14 Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Mon, 4 May 2026 14:10:22 +0200
Subject: [PATCH 11/14] remove space, add simp lemma, simplify

---
 Mathlib/RingTheory/DedekindDomain/Factorization.lean  | 11 +++++++----
 .../UniqueFactorizationDomain/NormalizedFactors.lean  |  2 +-
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index 72caa23824ca89..a1e3d9a6817ae6 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -902,6 +902,11 @@ These are phrased in terms of `multiplicity p.asIdeal I`.
 
 section multiplicity
 
+@[simp]
+lemma emultiplicity_bot {R : Type*} [CommSemiring R] (I : Ideal R) :
+    emultiplicity I (⊥ : Ideal R) = ⊤ :=
+  Submodule.zero_eq_bot (R := R) (M := R) ▸ emultiplicity_zero I
+
 variable {R : Type*} [CommRing R] [IsDedekindDomain R]
 
 lemma Ideal.finprod_heightOneSpectrum_pow_multiplicity {I : Ideal R} (hI : I ≠ ⊥) :
@@ -932,11 +937,9 @@ variable (I J) in
 lemma emultiplicity_sup :
     emultiplicity p.asIdeal (I ⊔ J) = emultiplicity p.asIdeal I ⊓ emultiplicity p.asIdeal J := by
   rcases eq_or_ne I ⊥ with rfl | hI
-  · rw [bot_eq_zero, emultiplicity_zero]
-    simp
+  · simp
   rcases eq_or_ne J ⊥ with rfl | hJ
-  · rw [bot_eq_zero, emultiplicity_zero]
-    simp
+  · simp
   have : I ⊔ J ≠ ⊥ := by grind
   have H {I' : Ideal R} (h : I' ≠ ⊥) : FiniteMultiplicity p.asIdeal I' :=
     FiniteMultiplicity.of_prime_left (prime p) h
diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
index 53b75fbe6e03a7..0287a63fe69abc 100644
--- a/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
+++ b/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
@@ -406,7 +406,7 @@ end UniqueFactorizationMonoid
 
 namespace UniqueFactorizationMonoid
 
-open  Multiset
+open Multiset
 
 variable {α : Type*} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq α]
 

From 4f1f379cb55daed738edfc3a32a49f3a77d9d0dd Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Mon, 4 May 2026 15:51:29 +0200
Subject: [PATCH 12/14] namespace new lemma

---
 Mathlib/RingTheory/DedekindDomain/Factorization.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index a1e3d9a6817ae6..73efb5cacfd6d6 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -903,7 +903,7 @@ These are phrased in terms of `multiplicity p.asIdeal I`.
 section multiplicity
 
 @[simp]
-lemma emultiplicity_bot {R : Type*} [CommSemiring R] (I : Ideal R) :
+lemma Ideal.emultiplicity_bot {R : Type*} [CommSemiring R] (I : Ideal R) :
     emultiplicity I (⊥ : Ideal R) = ⊤ :=
   Submodule.zero_eq_bot (R := R) (M := R) ▸ emultiplicity_zero I
 

From c7add5ed8017ce06b1bca2db09009467de49af31 Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Mon, 4 May 2026 15:52:03 +0200
Subject: [PATCH 13/14] remove type ascription

---
 Mathlib/RingTheory/DedekindDomain/Factorization.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index 73efb5cacfd6d6..6161e855c2e4ec 100644
--- a/Mathlib/RingTheory/DedekindDomain/Factorization.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
@@ -903,8 +903,7 @@ These are phrased in terms of `multiplicity p.asIdeal I`.
 section multiplicity
 
 @[simp]
-lemma Ideal.emultiplicity_bot {R : Type*} [CommSemiring R] (I : Ideal R) :
-    emultiplicity I (⊥ : Ideal R) = ⊤ :=
+lemma Ideal.emultiplicity_bot {R : Type*} [CommSemiring R] (I : Ideal R) : emultiplicity I ⊥ = ⊤ :=
   Submodule.zero_eq_bot (R := R) (M := R) ▸ emultiplicity_zero I
 
 variable {R : Type*} [CommRing R] [IsDedekindDomain R]

From 121160758e9049fe91b742eea92a9b1c277902b4 Mon Sep 17 00:00:00 2001
From: Michael Stoll <Michael.Stoll@uni-bayreuth.de>
Date: Wed, 6 May 2026 17:48:19 +0200
Subject: [PATCH 14/14] add lemmas on finite places

---
 Mathlib/NumberTheory/NumberField/Basic.lean    |  4 ++++
 .../NumberField/Completion/FinitePlace.lean    | 18 ++++++++++++++++++
 2 files changed, 22 insertions(+)

diff --git a/Mathlib/NumberTheory/NumberField/Basic.lean b/Mathlib/NumberTheory/NumberField/Basic.lean
index f9a421bd655e33..e1053610428dfa 100644
--- a/Mathlib/NumberTheory/NumberField/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/Basic.lean
@@ -59,6 +59,10 @@ variable (K L : Type*) [Field K] [Field L]
 -- See note [lower instance priority]
 attribute [instance] NumberField.to_charZero NumberField.to_finiteDimensional
 
+lemma one_le_finrank_rat [NumberField K] : 1 ≤ Module.finrank ℚ K := by
+  rw [Nat.one_le_iff_ne_zero, Ne, Module.finrank_eq_zero_iff_of_free]
+  exact not_subsingleton K
+
 protected theorem isAlgebraic [NumberField K] : Algebra.IsAlgebraic ℚ K :=
   Algebra.IsAlgebraic.of_finite _ _
 
diff --git a/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean b/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
index 0124b74fc8c4f1..296f0b9063cacc 100644
--- a/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
+++ b/Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean
@@ -359,12 +359,19 @@ noncomputable def equivHeightOneSpectrum :
   left_inv := mk_maximalIdeal
   right_inv := maximalIdeal_mk
 
+lemma equivHeightOneSpectrum_apply (v : FinitePlace K) :
+    v.equivHeightOneSpectrum = v.maximalIdeal := rfl
+
 lemma maximalIdeal_injective : (fun w : FinitePlace K ↦ maximalIdeal w).Injective :=
   equivHeightOneSpectrum.injective
 
 lemma maximalIdeal_inj (w₁ w₂ : FinitePlace K) : maximalIdeal w₁ = maximalIdeal w₂ ↔ w₁ = w₂ :=
   equivHeightOneSpectrum.injective.eq_iff
 
+lemma asIdeal_maximalIdeal_injective :
+    (fun v : FinitePlace K ↦ v.maximalIdeal.asIdeal).Injective :=
+  fun ⦃_ _⦄ h ↦ (FinitePlace.maximalIdeal_inj ..).mp <| HeightOneSpectrum.ext h
+
 @[fun_prop]
 theorem hasFiniteMulSupport_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) :
     (fun w : FinitePlace K ↦ w x).HasFiniteMulSupport := by
@@ -414,6 +421,17 @@ alias IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply :=
 @[deprecated (since := "2026-03-11")]
 alias IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm := embedding_mul_absNorm
 
+lemma finprod_finitePlace_pow_multiplicity {I : Ideal (𝓞 K)} (hI : I ≠ 0) :
+    ∏ᶠ v : FinitePlace K, v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal I = I := by
+  conv_rhs => rw [← finprod_heightOneSpectrum_pow_multiplicity hI]
+  simp only [← finprod_comp_equiv (equivHeightOneSpectrum (K := K)), equivHeightOneSpectrum_apply]
+
+lemma apply_mul_absNorm_pow_eq_one (v : FinitePlace K) {x : 𝓞 K} (hx : x ≠ 0) :
+    v x * v.maximalIdeal.asIdeal.absNorm ^ multiplicity v.maximalIdeal.asIdeal (span {x}) = 1 := by
+  have hnz : span {x} ≠ ⊥ := mt Submodule.span_singleton_eq_bot.mp hx
+  rw [← norm_embedding_eq v x, ← Nat.cast_pow, ← map_pow, ← maxPowDividing_eq_pow_multiplicity hnz]
+  exact HeightOneSpectrum.embedding_mul_absNorm K v.maximalIdeal hx
+
 end FinitePlace
 
 section LiesOver