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
diff --git a/Mathlib/RingTheory/DedekindDomain/Factorization.lean b/Mathlib/RingTheory/DedekindDomain/Factorization.lean
index f19e75dd949380..6161e855c2e4ec 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 multiplicities
+
+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`.
+-/
+
+section conversion
+
+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 :
+    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
+
+-- 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 :
+    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 :
+    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
+
+@[simp]
+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]
+
+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
+
+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 (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 prod_inter_normalizedFactors_ne_zero I J
+  rw [normalizedFactors_prod_inter_eq_inter]
+  exact count_inter ..
+
+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
+  · simp
+  rcases eq_or_ne J ⊥ with rfl | hJ
+  · 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
+
+variable {ι : Type*} [Finite ι]
+
+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 =>
+    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]
+    exact congrArg _ <| EquivLike.range_comp (emultiplicity p.asIdeal <| I ·) e
+  | h_option ih =>
+    rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
+
+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
+  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_iSup p I
+  simp only [H'.emultiplicity_eq_multiplicity, (H _).emultiplicity_eq_multiplicity] at this
+  exact_mod_cast this
+
+end IsDedekindDomain.HeightOneSpectrum
+
+end multiplicity
diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
index 4d240726072a2c..c9e2099acc9ef3 100644
--- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
+++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
@@ -401,31 +401,19 @@ theorem count_le_of_ideal_ge
 
 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
-      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
+    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_inter_eq_inter, le_iff_count]
+    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)
 
 @[deprecated (since := "2026-04-16")]
 alias _root_.sup_eq_prod_inf_factors := sup_eq_prod_inf_factors
diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
index 51460d4784ba57..0287a63fe69abc 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